00:00:35 OK 00:00:49 O.K. 00:01:23 For simplicity, XOR is [ A NAND ( A NAND B ) ] NAND 00:01:33 NAND logic and all that. 00:01:46 I think it's turing complete. 00:02:07 -!- heroux has quit (Ping timeout: 258 seconds). 00:02:17 I can prove turing completeness for half of all computable problems, but I don't have a proof of the others. 00:02:47 Specifically, problems with odd numbers of instructions are the issue. 00:02:54 Any ideas on how to prove it? 00:04:04 -!- Umbrage has quit (Remote host closed the connection). 00:18:58 -!- heroux has joined. 01:04:25 -!- heroux has quit (Ping timeout: 264 seconds). 01:10:47 -!- heroux has joined. 01:16:50 -!- heroux has quit (Ping timeout: 265 seconds). 01:22:35 -!- heroux has joined. 02:01:14 -!- Phantom___Hoover has joined. 02:15:46 -!- craigo has joined. 02:30:39 -!- LKoen has quit (Read error: Connection reset by peer). 02:31:10 -!- LKoen has joined. 02:51:12 Why is the Adobe font metric format not like a PostScript format? I think the TeX font format is better. Some people say that METAFONT doesn't do outline fonts or hinting, but actually it does both. The mainly problem with TeX fornat is the limits, and the kerning/ligature programs can't look ahead more than one character, but the Adobe format seems to be similarly limited from what I can see. 02:52:13 -!- LKoen has quit (Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.”). 03:05:22 -!- Phantom___Hoover has quit (Ping timeout: 256 seconds). 03:09:33 -!- tromp has quit (Remote host closed the connection). 04:28:50 -!- MDude has quit (Ping timeout: 256 seconds). 04:58:53 This is the Magic: the Gathering major template for TeXnicard so far: http://zzo38computer.org/fossil/texnicard.ui/dir?ci=tip&name=templates/magic Do you have any comments/complaints of it please? 05:52:14 -!- tromp has joined. 05:56:56 -!- tromp has quit (Ping timeout: 246 seconds). 06:13:31 -!- tswett[m] has quit (*.net *.split). 06:13:31 -!- APic has quit (*.net *.split). 06:15:22 -!- tswett[m] has joined. 06:15:22 -!- APic has joined. 06:19:11 -!- batman_nair has joined. 06:21:11 -!- batman_nair has quit (Remote host closed the connection). 06:41:49 [[Truth-machine]] https://esolangs.org/w/index.php?diff=71227&oldid=71181 * YamTokTpaFa * (+112) /* Pxem */ 06:46:44 -!- tromp has joined. 06:51:13 -!- tromp has quit (Ping timeout: 272 seconds). 07:10:27 -!- tromp has joined. 07:36:47 -!- user24 has joined. 08:03:02 -!- kspalaiologos has joined. 08:25:41 [[Functasy]] https://esolangs.org/w/index.php?diff=71228&oldid=65706 * Hakerh400 * (+7289) Add better highlighting 08:31:50 -!- heroux has quit (Ping timeout: 265 seconds). 08:38:21 -!- heroux has joined. 09:01:15 [[Ral]] https://esolangs.org/w/index.php?diff=71229&oldid=68419 * Herman-L * (+1436) 09:02:25 -!- batman_nair has joined. 09:28:43 -!- heroux has quit (Read error: Connection reset by peer). 09:29:34 -!- heroux has joined. 09:37:30 -!- heroux has quit (Read error: Connection reset by peer). 09:45:01 -!- heroux has joined. 09:48:50 -!- Lord_of_Life has quit (Ping timeout: 256 seconds). 09:50:29 -!- Lord_of_Life has joined. 10:00:27 [[Babalang]] https://esolangs.org/w/index.php?diff=71230&oldid=71119 * RocketRace * (+2291) Document GROUP 10:03:16 [[User talk:RocketRace]] M https://esolangs.org/w/index.php?diff=71231&oldid=71105 * RocketRace * (+161) 10:03:25 -!- Phantom___Hoover has joined. 10:03:35 -!- rain1 has joined. 10:16:13 -!- batman_nair has quit (Quit: Leaving). 10:16:19 -!- imode has quit (Ping timeout: 260 seconds). 10:31:47 -!- mra90 has left ("Leaving"). 10:54:00 [[Babalang]] https://esolangs.org/w/index.php?diff=71232&oldid=71230 * RocketRace * (+4447) Document LEVEL and IMAGE 10:57:00 [[Babalang]] https://esolangs.org/w/index.php?diff=71233&oldid=71232 * RocketRace * (+225) Document EMPTY 10:57:53 Hah @xkcd. 10:58:24 . o O ( So... statistics is the art of refining garbage into something resembling reliable data. ) 10:58:27 `? statistics 10:58:30 statistics? ¯\(°​_o)/¯ 11:01:21 hi 11:05:05 `lear Statistics is the art of refining garbage into data. 11:05:08 lear? No such file or directory 11:05:08 `learn Statistics is the art of refining garbage into data. 11:05:14 Learned 'statistic': Statistics is the art of refining garbage into data. 11:05:25 (I think it's passable. Feel free to improve.) 11:05:39 Or would that be s/improve/refine/ ;-) 11:12:50 -!- LKoen has joined. 11:23:27 fungot, what kind of video games do you play? 11:23:27 b_jonas: are any of you have a copy? 11:23:34 fungot: a copy of what? 11:23:35 b_jonas: to, even. doesn't that count for something. 11:25:41 fungot: it it's even it may be two. 11:25:41 int-e: that's just wrong. 11:25:52 fungot: I'm sorry you think that. 11:25:52 int-e: that only accepts a bf interpreter that takes i/ o 11:32:37 -!- heroux has quit (Ping timeout: 264 seconds). 12:01:14 [[Babalang]] https://esolangs.org/w/index.php?diff=71234&oldid=71233 * RocketRace * (+8156) Document the entire god damn runtime 12:07:35 [[Babalang]] https://esolangs.org/w/index.php?diff=71235&oldid=71234 * RocketRace * (+8199) Add examples (oh no......) 12:09:02 [[Language list]] M https://esolangs.org/w/index.php?diff=71236&oldid=71191 * RocketRace * (+15) Add Babalang 12:12:15 [[Babalang]] https://esolangs.org/w/index.php?diff=71237&oldid=71235 * RocketRace * (+100) Categorize the page 12:12:52 [[Babalang]] M https://esolangs.org/w/index.php?diff=71238&oldid=71237 * RocketRace * (-8) Change wording in description 12:13:10 [[Babalang]] M https://esolangs.org/w/index.php?diff=71239&oldid=71238 * RocketRace * (-4) Fix broken link 12:33:52 [[User:PythonshellDebugwindow/Cmt]] M https://esolangs.org/w/index.php?diff=71240&oldid=71222 * PythonshellDebugwindow * (+19) 13:00:26 -!- arseniiv has joined. 13:26:49 [[Welcome To...]] N https://esolangs.org/w/index.php?oldid=71241 * PythonshellDebugwindow * (+2108) Work in progress 13:38:51 -!- heroux has joined. 13:53:37 -!- heroux has quit (Ping timeout: 264 seconds). 13:54:06 -!- kspalaiologos has quit (Quit: Leaving). 13:54:11 -!- heroux has joined. 14:58:03 -!- Elderberry has joined. 14:58:17 Anyone online? 14:59:38 yeah 14:59:55 -!- rain1 has quit (Quit: Lost terminal). 15:42:09 -!- Cale has quit (Remote host closed the connection). 15:45:39 -!- Cale has joined. 16:04:34 [[User:Willicoder]] https://esolangs.org/w/index.php?diff=71242&oldid=71148 * Willicoder * (+265) 16:08:04 -!- Elderberry has quit (Remote host closed the connection). 16:08:33 [[Functasy]] https://esolangs.org/w/index.php?diff=71243&oldid=71228 * Hakerh400 * (+25) Fix typo in the code 16:27:13 -!- imode has joined. 16:38:06 -!- rain1 has joined. 16:55:54 -!- ais523 has joined. 16:56:21 for everyone who doesn't know how UTF-7 works: all of ASCII encodes itself apart from the "+" character, which is encoded in UTF-7 as "+-" 16:56:28 and then sequences starting with + are used for non-ASCII characters 16:57:22 Thanks for the Explanation! 16:57:23 I'm not 100% sure on the encoding after the +, but if I'm remembering correctly, it's just UTF-16 written in hexadecimal 16:57:47 (terminated by - if the next character is a hexadecimal character or -, or with no explicit terminator if it's outside the hexadecimal range) 16:58:27 that sounds really inefficient 16:58:37 that's probably why it didn't catch on 16:59:17 the main design goal appears to have been that a recipient could guess what it meant even if they didn't know the format, but that possibly isn't a useful design goal 17:00:13 -!- craigo has quit (Ping timeout: 264 seconds). 17:00:42 ah no, it isn't hexadecimal, it must be something more efficient than that 17:00:48 maybe base64'd utf-16? 17:01:03 I just encoded a BOM into utf-7, it encoded as +/v8- 17:01:21 it's a base64 variant wedeged between + and -. 17:01:21 `` echo '/v8' | base64 -d | od -t x1z 17:01:23 base64: invalid input \ 0000000 fe ff >..< \ 0000002 17:01:29 yes, that looks like base64 to me 17:01:48 (With the +- exception that maps to + as you said) 17:02:13 base64 is still a bit inefficient but it isn't as inefficient as base16 17:02:55 now I wonder how many editors will interpret files as UTF-7 if they start +/v8 followed by - or a non-base-64 character 17:02:59 probably not many 17:03:29 'Older versions of Internet Explorer can be tricked into interpreting the page as UTF-7. This can be used for a cross-site scripting attack as the < and > marks can be encoded as +ADw- and +AD4- in UTF-7, which most validators let through as simple text.' 17:03:42 So it did have serious applications :P 17:03:58 oh right, IE 17:04:08 I seem to remember someone managing an XSS attack against the #esoteric logs 17:04:17 because IE was so permissive with encodings and MIME types 17:04:44 And yes, it stacks on top of UTF-16. What a mess. 17:05:56 I still think that, in a way, it's a pity that UTF-1 didn't catch on 17:06:32 the rise of UTF-8 caused serious standards incompatibility problems, because UTF-8 uses C1 control codes for purposes other than their assigned meanings 17:07:28 although, given that a C1 control code cannot appear in UTF-8 except immediately after a G1 character, this ambiguity should be fixable, but nobody I know of but me actually tries to fix it 17:09:19 I guess part of the problem is that many of the C1 control codes are kind-of silly 17:11:52 -!- tromp has quit (Remote host closed the connection). 17:31:01 -!- tromp has joined. 17:33:27 -!- Lord_of_Life has quit (Read error: Connection reset by peer). 17:33:54 -!- Lord_of_Life has joined. 17:35:57 -!- tromp has quit (Ping timeout: 272 seconds). 18:01:35 oh nice. that's like the XSS attacks when a browser guesses that something is HTML even though the HTTP response header Content-Type says text/plain 18:12:33 This encoding is a bit inefficient but it seems OK. 18:12:43 The one that I don't get is Punycode. What's with that? It seems so complicated. 18:16:39 Yeah, Punycode is pretty awful. It seems to be designed for a language like German where words are mostly ASCII with maybe one or two non-ASCII characters. 18:17:29 "Punycode is a simple and efficient transfer encoding syntax [...]" 18:17:30 But even so, it seems completely unreadable by humans. 18:17:59 unreadable by humans, annoying to implement.. 18:18:07 I don't agree with this use of the word "simple". 18:18:52 `` python -c 'print([s.encode("punycode") for s in ["aaa", "aaaλ", "aaaaλ", "aaaλbbb"]])' 18:18:53 ​['aaa-', 'aaa-3ga8g', 'aaaa-tia7i', 'aaabbb-5la5m'] 18:19:11 thunycode 18:19:25 shachaf: Well one can kind of guess what "Mnchen-3ya" stands for. 18:19:41 But not by knowing anything about the string "3ya"! 18:19:53 Sure. 18:19:56 Welcome back btw. 18:20:10 You might as well write "M�nchen". 18:20:33 (Except it doesn't even tell you where the replacement character is.) 18:20:44 You might not have to implement Punycode, at least. 18:20:54 I'm probably only sort of back? Hard to say. 18:21:09 How do you meant only sort of back? 18:21:12 The only good thing about punycode is that you generally don't see it in encoded form. 18:22:27 How about this Punycode replacement: You write "m-nchen--fc.com" for "münchen.com". 18:23:17 Each code point above 127 and - gets encoded as a -, and then they're listen in order in hexadecimal after the -- 18:23:22 That's probably not very good. 18:23:29 Too verbose. 18:23:57 `` python -c 'print([s.encode("punycode") for s in ["привет"]])' 18:23:58 It helps since you can write domain names purely in the ASCII form. You can disable non-ASCII domain names and then it will still work, and avoid the homoglyph problems and missing fonts and so on, too. 18:23:58 ​['ae7lman4b1hcbbfh'] 18:25:11 However, I should think they should not have needed support for domain names containing any characters not already valid in domain names anyways 18:26:26 shachaf: I guess there's one advantage to punycode that's easy to miss: some character set restrictions (like domain names not containing dots) can be enforced on punycode encoded strings without decoding them 18:26:47 But overall it doesn't seem very nice. 18:27:08 How does that work? 18:28:21 the . would become part of the unencoded base character sequence before the final minus sign 18:30:08 (This is assuming that base characters can't be encoded in the final encoded part, which I believe is the case.) 18:30:25 So you mean it doesn't have an equivalent of overlong encodings of ASCII characters. 18:30:33 Right. 18:30:42 -!- tromp has joined. 18:31:18 But you can still have encoding errors, right? Overlong encodings are already an error in UTF-8. 18:32:50 I suppose so 18:32:54 -!- tromp_ has joined. 18:33:12 But I don't know for sure. 18:33:28 (I'm not interested enough to check this in detail.) 18:34:17 I'm now reading about how Punycode actually works and it's kind of ridiculous. 18:34:30 `` python -c 'print([s.encode("punycode") for s in ["München"]])' 18:34:31 ​['Mnchen-bma9c'] 18:36:45 -!- tromp has quit (Ping timeout: 272 seconds). 18:37:22 It is kind of neat if you like arithmetic coding. 18:37:26 [[User:PythonshellDebugwindow/Stub]] N https://esolangs.org/w/index.php?oldid=71244 * PythonshellDebugwindow * (+26) Created page with "Leave this page as a stub." 18:38:07 I guess it's pretty efficient, at least. 18:38:31 [[Esolang:Sandbox]] M https://esolangs.org/w/index.php?diff=71245&oldid=70695 * PythonshellDebugwindow * (+228) 18:43:24 [[A]] M https://esolangs.org/w/index.php?diff=71246&oldid=68569 * PythonshellDebugwindow * (+153) /* External links */ 18:43:29 `` python -c 'print([s.encode("punycode") for s in ["bücher"]])' 18:43:30 ​['bcher-lka2c'] 18:43:45 What' going on there? Is it normalizing the Unicode into two characters before encoding or something? 18:44:04 `` python -c 'print([s.encode("punycode") for s in ["bücher"]])' 18:44:06 ​['bucher-xba75c'] 18:44:22 [[Ellipsis]] M https://esolangs.org/w/index.php?diff=71247&oldid=63411 * PythonshellDebugwindow * (+76) cats 18:44:43 Oh, of course it's not. 18:45:16 Oh, it's a Python 2 thing, isn't it. 18:45:35 `` py 18:45:36 ​/hackenv/bin/`: line 5: py: command not found 18:45:41 `` python3 -c 'print([s.encode("punycode") for s in [u"bücher"]])' 18:45:42 ​[b'bcher-kva'] 18:47:10 `` python3 -c 'print([s.encode("punycode") for s in ["ü"]])' 18:47:11 ​[b'tda'] 18:47:25 okay I don’t get punycode at all 18:47:53 > foldr (\x y -> x + y * 36) 0 $ map (\d -> fromJust $ elemIndex d (['a'..'z'] ++ ['0'..'9'])) "tda" 18:47:55 127 18:48:06 ah, and I think I first thought that’s the same as what urlencode does 18:48:41 `` python3 -c 'print([s.encode("punycode") for s in ["ü"]])' 18:48:42 ​[b'u-ccb'] 18:49:18 > text [chr (127 + 125)] 18:49:20 ü 18:49:49 ah, so it seeingly first prefixes all ASCII codepoints from the string, if any, and then base-something-encoded string in full 18:50:01 though I might have read about it already somewhere 18:50:50 `` python3 -c 'print([s.encode("punycode") for s in ["aμb⚁cъd"]])' 18:50:51 ​[b'abcd-lnd86f056o'] 18:52:03 It encodes the code points and positions in base 36. 18:56:36 ah, now I have read a part of discussion above too :D should have done that earlier 19:06:59 ais523: also that's why we don't allow overlong encodings in UTF-8 19:24:41 For some applications, overlong encodings in UTF-8 is useful 19:25:41 Exploiting buggy software, for instance? 19:29:37 Maybe, although that isn't what I meant. 19:52:01 -!- tromp_ has quit (Remote host closed the connection). 20:04:18 -!- tromp has joined. 20:06:15 -!- rain1 has quit (Quit: Lost terminal). 20:07:42 [[Fish]] M https://esolangs.org/w/index.php?diff=71248&oldid=59315 * PythonshellDebugwindow * (+4) /* FizzBuzz */ add link 20:08:29 [[User:Hakerh400]] M https://esolangs.org/w/index.php?diff=71249&oldid=70998 * Hakerh400 * (+0) Reorder sections 20:11:17 b_jonas: I think encoding NUL as 00 in UTF-8 was a mistake 20:11:33 ais523: why? 20:11:42 I would prefer an encoding of C0 80, to allow an "out-of-band" string termination character 20:12:12 In some applications you can use C0 80 to encode a null character in a UTF-8 string, to use 00 as a string termination. But in other cases you don't do that. 20:12:43 ais523: you can always define a custom escaping transform, that should be independent of the encoding itself. you can even use 0x80 or 0x81 20:13:26 ais523: I don't usually trust that strings that claim to be utf-8 are really valid utf-8 anyway, so I wouldn't trust that they don't have a 0x00 or 0x80 or whatever 20:13:38 b_jonas: I would also prefer that C1 control codes are encoded as themselves, but that's more controversial (the encoding is still self-synchronizing but to a lesser extent) 20:14:26 Maybe programs I write I design to use ASCII and not Unicode, anyways 20:15:45 hmm, that reminds me, I came up with a binary format that has similar purposes to JSON, in which all strings encoded themselves (in UTF-8), and all nonstrings used invalid UTF-8 sequences 20:16:17 -!- arseniiv_ has joined. 20:19:24 Can you encode surrogates if needed? 20:19:28 -!- arseniiv has quit (Ping timeout: 256 seconds). 20:19:46 (You might need it if the data isn't Unicode, for example.) 20:21:10 And then, what about characters beyond the range of Unicode? 20:22:36 Do you have the documentation for your format? 20:23:26 -!- LKoen has quit (Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.”). 20:24:29 zzo38: http://nethack4.org/pastebin/gsap.txt 20:25:45 I think out-of-range characters and surrogates can be encoded in the format, but the format is meant to disallow them because strings are meant to be Unicode only 20:26:01 if you have a string of character-like things that is not Unicode, it should probably be stored as an array of bytes 20:27:25 also I think there's a missing " in the example near the start 20:27:28 I haven't looked at this file for ages 20:31:12 I do not see anything about byte arrays; also, it doesn't seems to be able to use lists of exactly one element when dynamic types are used, from what I can tell. 20:31:56 a list of one element is equivalent to the element itself 20:32:06 and a byte array would be represented as a nonliteral containing the bytes as arguments 20:32:19 e.g. (bytes 2 12 255 0 255) 20:32:39 this is intended for use with schemas / strong typing, so you can always distinguish a singleton list from an element 20:32:54 Yes, that is what I thought about a list of one element, but if a distinction is needed between lists and non-lists then that won't work when dynamic types are used. 20:33:37 It says the format can be either statically or dynamically typed. With static types what you say will work, for the reason you mention, but that won't work so well for dynamic types, I think. 20:34:48 well, there are two ways to think about dynamic typing 20:35:16 IMO in a dynamically typed language, you should just treat the data as whatever type you're expecting it to have, and not care about what type it actually has 20:35:26 Also, the byte arrays done in the way like you mention does not seem to be efficient. 20:37:07 ais523: that's perl typing or dwim scalars 20:37:53 zzo38: yes, but this is a very uncommon use case 20:38:17 b_jonas: yes, it's the only sensible way to do dynamic typing I think 20:38:22 the other method is to write programs sort of like in a strongly typed language, except you omit some enum constructors in favor of storing multiple types and checking for them, mostly with a nul type versus other types, or an array versus a number 20:38:36 and I prefer that style 20:38:41 well, that and stringly typing, where everything is stored as a string (or else in some format that isn't a string but acts like one) 20:38:54 yes, there's that too 20:39:09 b_jonas: I think that style is kind-of terrible unless you have a huge supply of enum constructors that can just be used anywhere 20:39:19 and do in fact use them everywhere 20:39:39 "this function takes a string or an integer" is horrible in terms of self-documentation, and can't easily be modified into taking a string or a different type of string 20:40:14 For storing structured data which does not need to be parsed into other data structures after it is read, I like the format http://fileformats.archiveteam.org/wiki/PostScript_binary_object_format but it has the disadvantage that, unlike your format, it does not support streaming writing, and will require two passes to write. 20:41:02 ais523: what do you call the kind of typing that x86 machine language or forth does, which isn't dynamic typing because there are no type tags in data, but also no type information at compile time? 20:41:41 b_jonas: "everything is just bits" 20:41:46 I'm not sure if it has a proper name beyond that 20:42:25 hmm, actually I think this conversation has helped me clarify my understanding: type tags in data that just store the type rather than the meaning are about as useful as Hungarian notation that just stores the type rather than the meaning 20:42:59 occasionally it helps, but only in programs where each type can only have one possible meaning, which is rare 20:43:20 Another format is RELOAD, which also supports efficient byte arrays like PostScript does, but that is with another different use. In RELOAD, all names are indicated by numbers, and which names correspond to which numbers is listed at the end. Although it requires parsing, it allows a program to write out using its own numbers, while when reading it can efficiently create a table mapping the file's numbers to its internal numbers. 20:45:20 the gsap format I linked, the main motivation was to be able to implement most parser-like operations using only a single stack, + an append-only output 20:45:33 to make the best possible use of memory bandwidth and cache 20:45:41 ais523: is it "everything is just bits" even if you aren't manipulating bytes or fixed-size words, but nonnegative bignums such as in Amicus? 20:46:00 b_jonas: well, the bignum is also just bits 20:46:07 you have to know it's a bignum some other way to be able to operate on it correctly 20:46:16 ais523: Yes, it does have those advantages at least. 20:47:10 ais523: well it is manipulated in binary 20:49:13 ais523: meaning of the data => yes, which is some modern dynamically typed languages are object-oriented. 20:50:35 anyway I find that in practice, Python or JavaScript programs nearly always are only meant to allow one type in each function argument / variable 20:50:57 and this has to be documented and verified to always be the case by humans (or via some sort of typing extension to the language) 20:51:20 so the dynamic typing mostly just serves to increase the risk of bugs and increase the amount of manual effort 20:51:23 I quite like python's type system: objects have a class, which you can imagine as if all objects (except maybe small integers) have a class pointer in them, and the class determines the representation of the rest of that object, as in what fields it has for normal objects, or whether it's a variable sized object like tuple or bytes or str that has an variable sized array allocated inside the object (so 20:51:29 it can't be resized). 20:51:49 whereas if you're using Perl-style typing, it's very hard to get wrong because you can't accidentally pass a string rather than an integer or the like 20:51:57 the actual representation could differ, this is just the notion 20:52:08 ais523: There are some exceptions though, sometimes I do use support for multiple types in a variable/argument although usually it is only one type. Especially if it accepts null in addition to another type. 20:52:15 the basical problem here is to do with references, which are a fundamentally different thing from strings and integers 20:52:32 and you can define new classes, and either you tell what fields they have, or you inherit from a class with one of those special variable sized representation. 20:52:33 Another case in JavaScript is sometimes a function might accept either a string or a byte array; this is used in Node.js to represent file names, for example. 20:52:54 zzo38: "null or X" arguments have been a huge source of bugs historically, though; most modern programming languages use some techniques to ensure that nullability is always clear, and that the null case is handled if it could happen 20:53:16 it's very easy to write a function where some input could be null but the programmer didn't realise it while writing the function 20:54:04 ais523: Yes; if you are using Haskell then you can use Maybe, although in JavaScript programs at least, I write it the way I need and it still works anyways. 20:54:48 in any case, you can use python's class-object system to write programs where your functions accept many different types if you want 20:58:31 I am now trying to write a specification of a change set format for TeXnicard, which is intended to be readable ASCII text which can be included in netnews articles. 21:00:30 Do you have any comments about doing such a thing? 21:17:51 Well, do it 20 years ago... 21:20:10 I can't do it 20 years ago; I will do it now. It won't be useful to do it before TeXnicard is written, anyways. 21:21:29 zzo38: do TeXnicard 20 years ago too 21:22:36 Well, I cannot do that, so I will have to do it now, instead. 21:27:06 -!- Phantom___Hoover has quit (Ping timeout: 265 seconds). 21:34:08 int-e: TODOs at 36 completed manually. so BB(36) = Church 2^256 is proven modulo bugs in BB.lhs 21:35:46 some TODOs could be eliminated if we can have H ::= □ | \v. H | H T | freeV H and B^V ::= W^V X^V | \v. B^V | B^V T | freeV B^V 21:39:57 -!- user24 has quit (Quit: Leaving). 21:43:59 tromp: that's probably fine 21:44:55 thanks for probable blessing:-) 21:49:45 -!- Lord_of_Life_ has joined. 21:50:55 -!- Lord_of_Life has quit (Ping timeout: 250 seconds). 21:52:11 tromp: you can generalize that a bit further to freeV T^* H 21:52:35 -!- Lord_of_Life_ has changed nick to Lord_of_Life. 21:52:42 (that * is replication, not function iteration) 21:53:02 -!- tromp_ has joined. 21:55:15 oh, good point, a normal form normalizes all arguments of a free variable 21:56:45 -!- tromp has quit (Ping timeout: 265 seconds). 22:09:13 Here is my document for TeXnicard change set format: http://zzo38computer.org/fossil/texnicard.ui/artifact/7fd7e8d9db30a7ca or http://zzo38computer.org/fossil/texnicard.ui/raw/changeset.doc?name=7fd7e8d9db30a7ca2cb46cc5b0e3c03e064f7173 Now you can see if it is good or not, and what comment you have of it. 23:50:29 -!- arseniiv_ has changed nick to arseniiv. 23:50:31 -!- imode has quit (Ping timeout: 250 seconds). 23:55:22 -!- arseniiv has quit (Ping timeout: 256 seconds).