< 1760662771 620882 :ajal!~ambylastn@host-92-17-32-126.as13285.net QUIT :Remote host closed the connection < 1760663564 438464 :Hooloovoo!~Hooloovoo@hax0rbana.org NICK :Hoolooboo > 1760669785 775447 PRIVMSG #esolangs :14[[07User:EZ132/Not C++14]]4 10 02https://esolangs.org/w/index.php?diff=166160&oldid=166149 5* 03EZ132 5* (+14) 10/* Design & History */ < 1760670273 1306 :lynndotpy60!~rootcanal@134.122.123.70 QUIT :Quit: bye bye < 1760670340 25818 :lynndotpy609!~rootcanal@134.122.123.70 JOIN #esolangs lynndotpy :lynn < 1760674376 722210 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :Can't say I've done much myself. Interesting choice of venue though < 1760674646 401789 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :It's been something of a reaction to (a) the uncomputability of many of the facts under study, combined with (b) the open refusal of some famous folks to not consider a GitHub repo to be citable even when it has working Coq proofs. < 1760674862 776494 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :the IRC channel and the wiki don't seem like an improvement there < 1760674921 109206 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Yeah, but that's why I've got my own GitHub repo. And the repo does render nicely into a readable format: https://bbgauge.info/ < 1760674959 685758 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :a GitHub repo isn't a valid source, so we add another GitHub repo? < 1760674998 82983 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Hey, I never said that I was smart, only that I'm willing to put in the work~ < 1760675140 70949 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :and a little curious what does and doesn't count as an "esolang" < 1760675141 425724 :ais523!~ais523@user/ais523 PRIVMSG #esolangs : the open refusal of some famous folks to not consider a GitHub repo to be citable even when it has working Coq proofs. ← I'm sort-of the opposite in that respect, in my PhD I intentionally tried to avoid citing things that weren't publicly available and pick publicly available alternatives < 1760675177 545689 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :sorear: defining "esolang" is difficult, a good working definition is that a language is esoteric if being useful to practically program in is not a design goal < 1760675199 570952 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :although I think that definition is slightly too restrictive < 1760675228 559145 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :I recently re-explained my definition, based on inclusionism vs deletionism, in the context of that one paper that went around: https://lobste.rs/s/ksrmbf/let_s_take_esoteric_programming#c_0gsmih < 1760675296 138940 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :nql was a means to an end so it fails that test < 1760675398 945251 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :I am thinking of Waterfall Construction Kit, a language I designed to write one program – I wrote the program and compiled it by hand without ever working out what the Waterfall Construction Kit specification was, and then abandoned the language it was written in < 1760675409 129977 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Well, maybe the ends aren't practical. NQL or bfmacro are great for producing programs for low-level machines that don't physically exist. They can be ergonomic while addressing problems in pure maths. An extreme example of that might be https://esolangs.org/wiki/Sammy which isn't known to be computable. < 1760675411 189340 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :is that an esolang? < 1760675435 297600 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :I guess both the "esoteric" and "language" halves of that are debatable! < 1760675486 765129 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :something like solidity comes to mind < 1760675511 438775 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :hmm, I just realised there's a sort of implicit assumption of "a programming language that is only useful when used with esolangs is an esolang" that I've never questioned before < 1760675522 455893 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :which _does_ have massive corporate backing, but I'm uncomfortable defining things strictly in terms of context < 1760675578 16962 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :I actually haven't looked at what solidity is like as a language, I kind-of assumed it was a relatively normal low-level VM, the same sort of thing as webassembly or the JVM, but I might be completely wrong < 1760675702 679425 :zzo38!~zzo38@host-24-207-46-238.public.eastlink.ca PRIVMSG #esolangs :I think that git repositories (hosted on GitHub or something else) can be citable, although when citing something that can be changed then it might be worth to specify what version; in the case of git you can specify the commit hash, and that might also help in case it is mirrored to something else then you can also find the matching commit hash. < 1760675702 910530 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Eye of the beholder, I guess; all three of those VMs are bonkers as compilation targets. I never did figure out how to compile Cammy to WASM in a satisfying way, nor Monte on JVM, although maybe I just didn't try very hard. < 1760675723 637355 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :after looking it up, it seems that I confused the VM (which is called EVM) with the language (Solidity) commonly used to compile to it < 1760675743 348606 :zzo38!~zzo38@host-24-207-46-238.public.eastlink.ca PRIVMSG #esolangs :Citing something that is publicly available is also good, rather than something that is not publicly available because then you could not easily check the citation if it is not public < 1760675743 508870 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :korvo: one of my recent pet theories is that everyone is doing IRs incorrectly < 1760675801 348727 :zzo38!~zzo38@host-24-207-46-238.public.eastlink.ca PRIVMSG #esolangs :Do you know what is the proper way to do IRs? < 1760675826 525485 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :I think the most important thing I would change would be to separate out UB from everything else: there would be an assert/assume instruction that defines circumstances to be UB, and all the other commands would be well-defined (although the definition could in some cases be "whatever the hardware does" for things like writing dangling pointers) < 1760675871 957452 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :that way, optimisations never cause you to lose track of what your UB assumptions are < 1760675885 112992 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :because you can preserve them as you optimise the code around them < 1760675890 924493 :zzo38!~zzo38@host-24-207-46-238.public.eastlink.ca PRIVMSG #esolangs :I think that would be reasonable, for that and possibly other reasons too < 1760675902 49128 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :this also means that if you want defined behaviour in a particular case, you can just remove the UB assumption you'd normally emit < 1760675933 987075 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :the problem with "dangling and out of range pointers do whatever the hardware does" is that it prevents optimizations that affect things that shouldn't be visible but can be made visible by pointer misuse, like stack frame layout and slot reuse < 1760675937 791794 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :zzo38: Yeah. In the case of Busy Beaver research, the problem is that our person doesn't really want to verify the artifacts in the repo; they want "either a prose writeup explaining what was done or independent verification of its correctness", quoting https://scottaaronson.blog/?p=9152#comment-2016433 < 1760675969 118693 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :this came up in the cakeml stack < 1760676003 239624 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :So in the case of e.g. Leng 2024, they would prefer that somebody who isn't Leng (me?) run the Coq proofs and confirm that they pass. I did that! But where do I put the prose so that it's acceptable? < 1760676036 744777 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :what exactly are the coq proofs? < 1760676087 113557 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Oh, not Leng, but mxdys; https://github.com/ccz181078/Coq-BB5 is the repo. Proofs of certain values of BB. < 1760676088 978527 :ais523!~ais523@user/ais523 PRIVMSG #esolangs : the problem with "dangling and out of range pointers do whatever the hardware does" is that it prevents optimizations that affect things that shouldn't be visible but can be made visible by pointer misuse, like stack frame layout and slot reuse ← that's why you have the UB assumptions – they permit that sort of optimization even though the rest of the IR doesn't < 1760676114 521356 :zzo38!~zzo38@host-24-207-46-238.public.eastlink.ca PRIVMSG #esolangs :It would help to have a proper prose writeup which is publicly available, in addition to the git repository, but if you do not have it then you will have to do what you do have, instead. < 1760676124 440951 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :ah, BB(small) < 1760676125 180825 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :They also don't acknowledge Leng's TM for Goldbach Conjecture, verified in Lean 4: https://github.com/lengyijun/goldbach_tm < 1760676126 409449 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :there is a writeup of that now, I think < 1760676163 389933 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :korvo: I bet they wouldn't acknowledge my 2-state 14-symbol universal TM < 1760676171 768979 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :which is written up half on esowiki and half on codegolf stack exchange < 1760676263 185045 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :ais523: Let's just say that there's a lot that Aaronson doesn't acknowledge, and leave it at that. Some of us think he's too biased elsewhere to be an acceptable primary source here. I'm still citing him properly for the contributions he's made. < 1760676317 764418 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :I don't appear to have your TM in the Gauge, either. Do you have a link? I can take a look now, and I'll open an issue on GitHub if it takes me more than a few days. < 1760676356 162094 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :anyway I think the gold standard for citing is "anything with a DOI" and the astro-ph people have a bunch of tools for turning code repos into something that can be cited < 1760676385 500182 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :OTOH it would be nice to have a complete explanation and not "here's 500 lines of python have fun" < 1760676461 309966 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :korvo: https://codegolf.stackexchange.com/questions/111278/turing-complete-language-interpreter/265539#265539 < 1760676467 668664 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Totally fair. My current standard is somewhere between "live link to a PDF" and "working Nix flake", but I think I'm a bit more of a hardscrabbler than a paper-writer. Certainly I haven't contributed anything of interest. < 1760676498 356316 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :it would be nice to have a proof for the zfc turing machines but there's a bunch of pieces to chain together, including the validity of the tarski-megill predicate calculus itself < 1760676511 449163 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :I wrote the Turing machine in question in 2019 but didn't prove it universal until 2023 (and the proof hasn't been peer-reviewed so it might be wrong) < 1760676537 602120 :zzo38!~zzo38@host-24-207-46-238.public.eastlink.ca PRIVMSG #esolangs :What is the DOI of a GitHub repository? Can you cite a specific version? < 1760676579 777691 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :you can definitely cite a particular version of a git repository, via providing the hash (which is, to any reasonable approximation, globally unique) < 1760676580 599924 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :ais523: Swag, thanks. I'll have to do more research to understand the previous champion that you mention, too. < 1760676611 132741 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :and GitHub allows for links that are tied to the git hash < 1760676624 799651 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :https://docs.github.com/en/repositories/archiving-a-github-repository/referencing-and-citing-content huh, there's Official Guidance now < 1760676660 401578 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :sorear: Something I've thought about a *lot*, and I presume you have too: what's the main obstacle to just implementing Metamath's Algorithm D as a low-level machine? That'd let us automatically compile quite a few interesting theories. < 1760676729 350726 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :I worry that proving that the cut-down algorithm is correct might be more effort than just proving that the implementation is actually Algo D. I also have an unhealthy desire for generalization. < 1760676793 864253 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :where is that defined? < 1760676925 548935 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Um, probably The Book, metamath.pdf. IIRC it comes from Meredith's work and Tarski showed its completeness. Might be misremembering the name; Meredith called it something like "algorithm of detached inference". < 1760676991 472233 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :meredith's work to the extent I remember was exclusively propositional calculus, which has limited computational relevance < 1760677055 899416 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :https://projecteuclid.org/journals/notre-dame-journal-of-formal-logic/volume-36/issue-3/A-Finitely-Axiomatized-Formalization-of-Predicate-Calculus-with-Equality/10.1305/ndjfl/1040149359.pdf p. 5 has D < 1760677124 531721 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :it's a unification process which requires parsing the wffs, intuitively seems far more complicated than the parsing-free approach < 1760677179 119940 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Yeah. But all of the parsing can be done at compile time; the actual unifications only have to proceed abstractly over some Herbrand structure, I think. < 1760677229 13071 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :I remember asking Mario something similar about whether we could mechanically extract a CFG from a Metamath database. IIRC he was like "yeah but why?" < 1760677372 763479 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :you still need to recursively/iteratively process terms, track used and unused variables, etc < 1760677462 653261 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :fundamentally it's a tool to allow maximum proof reuse through metavariables, but that's useless in a TM context so zf2.nql works purely with object variables and fully concrete formulas < 1760677524 899410 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :That's fair. My notes on proof search in ETCS are full of similar hacks, but I think I went too far; I convinced myself that ETCS is obviously consistent and now I don't know what to search for. < 1760677623 155554 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :I haven't done ETCC yet. If I figure out how to compute Sammy then maybe a Sammy interpreter would be smaller than ETCC contradiction search. < 1760677647 791022 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :But I don't know how to compute Kan extensions in general and it seems to be a bit of an open problem. < 1760677661 852452 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :what are the above? < 1760677711 879107 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :etcs/etcc/sammy; there's a wiki article for kan but i've always been terrible at categories < 1760677729 667723 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Category theory junk. ETCS is a theory of sets and functions; ETCS + Choice + Replacement is bi-interpretable with ZFC. ETCC is a theory of categories and functors, and Sammy's an esoteric language describing constructions in ETCC. < 1760677765 653405 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :No worries. I literally cannot hold a functor correctly; I'm always mixing up its variance and domains. < 1760677772 575408 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :zf2 _is_ general enough to express an arbitrary grammatically unambiguous metamath database with minor/"obvious" changes > 1760677846 309942 PRIVMSG #esolangs :14[[07User:None1/InDev14]]4 10 02https://esolangs.org/w/index.php?diff=166161&oldid=158865 5* 03None1 5* (+615) 10 < 1760678067 893355 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Yeah! I wouldn't ask if I didn't see it in the code history. I want to have a strong basis from which to evaluate CatsAreFluffy's work, since it seems like they're doing lots of small tweaks to the low-level proof statements without a high-level justification or verification. < 1760678252 665567 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :I figure that I won't know until I write more NQL, but did I miss anything when hacking out the wiki page? I got globals and procedures, natural numbers, assignments and lookups, if- and while-statements, and the history. < 1760678266 277893 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Oh! So I forgot arithmetic. < 1760678437 744010 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :the big improvement recently seems to be a switch from fixed length to variable length program counters, which is something I carefully considered before deciding it wasn't possible, my big goal is to understand what was actually done there < 1760678493 152598 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :it's a fairly boring algol/C clone (even has call by name!), if you caught the lisp, forth, and perl 6 references take a cookie < 1760678593 261495 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :there's if-decr and the builtin mechanism, not sure about "history" < 1760678717 997311 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :There's the 2016 theorem, the related language Laconic, and probably will be a new chapter after we get all of these new commits wrangled. < 1760678796 522988 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :ah, the history of nql as described in the wiki page, thought you were talking about "history" as an internal feature of the language < 1760678828 340034 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Oh, ha, sorry. Bad with words tonight. < 1760678995 948552 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :i'll most likely merge the improvements if I manage to understand them < 1760679074 685662 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :part of the goal being to understand catsarefluffy's subprogram register machine well enough to explain it in prose < 1760679318 877916 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Cool. No rush. My goal is only to have a git commit that can build the rest of the book, and that can provide an apples-to-apples comparison of everybody's NQL programs. I don't want anybody's old code to be unfairly compared to somebody's new result just because of a compiler difference! < 1760679332 637959 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :book? < 1760679353 697437 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :The BB Gauge. It's basically a living book, even though it's just a cruddy little website. < 1760679387 992196 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Anyway, I have one commit that makes everything build for me, and I'll send that for review. < 1760679478 829488 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :I'll do what I can > 1760679908 648542 PRIVMSG #esolangs :14[[07Not-Quite-Laconic14]]4 10 02https://esolangs.org/w/index.php?diff=166162&oldid=164204 5* 03Corbin 5* (+803) 10/* Overview */ Document arithmetic and comparisons. (Everybody do the monus! The monus is a dance! Everybody is a genius! Who knows it in advance!) < 1760680115 626210 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :so recently a new user registered on the esowiki and wrote that they're interested in a language that I had documented. that means it's worth to document esoteric languages on the wiki. I'm just mentioning this just in case you ever despair about the state of the wiki and all the junk there is on < 1760680416 637765 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :b_jonas: I appreciate that, thanks. < 1760680481 572346 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :and they fixed a mistake where I documented that language incorrectly. or they introduced a mistake, I don't really know. > 1760680542 609349 PRIVMSG #esolangs :14[[07Not-Quite-Laconic14]]4 10 02https://esolangs.org/w/index.php?diff=166163&oldid=166162 5* 03Corbin 5* (+180) 10/* Procedures */ Document switch-statements somewhat. My understanding of the limitations here is from reading the grammar and AST. < 1760680583 892903 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :https://esolangs.org/w/index.php?diff=166111 < 1760680744 594538 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :hmm, that's incorrect < 1760680755 988241 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :they're not a new user, they wrote that they were interested in that language back in year 2022 > 1760680843 310691 PRIVMSG #esolangs :14[[07User:Zzo38/Untitled 214]]4 10 02https://esolangs.org/w/index.php?diff=166164&oldid=66278 5* 03Zzo38 5* (+71) 10 < 1760682342 271885 :Sgeo!~Sgeo@user/sgeo QUIT :Read error: Connection reset by peer < 1760686430 674159 :tromp!~textual@2001:1c00:3487:1b00:d983:2af2:5deb:9bbb JOIN #esolangs * :Textual User < 1760694898 482760 :chiselfuse!~chiselfus@user/chiselfuse QUIT :Remote host closed the connection < 1760694912 588672 :chiselfuse!~chiselfus@user/chiselfuse JOIN #esolangs chiselfuse :chiselfuse < 1760695278 293937 :APic!apic@apic.name PRIVMSG #esolangs :Hi * < 1760696027 845480 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :hmm, that complexity class argument on the NQL page – it's not completely obvious to me that ZFC being able to prove itself inconsistent implies that it actually *is* inconsistent < 1760696121 136768 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :(because it doesn't seem obviously necessary for it to have enough introspection to be able to get from there to a contradiction, and being able to prove false statements also doesn't imply that a system is inconsistent) < 1760700719 109206 :tromp!~textual@2001:1c00:3487:1b00:d983:2af2:5deb:9bbb QUIT :Quit: My iMac has gone to sleep. ZZZzzz… < 1760701002 947928 :Lord_of_Life_!~Lord@user/lord-of-life/x-2819915 JOIN #esolangs Lord_of_Life :Lord < 1760701003 814309 :Lord_of_Life!~Lord@user/lord-of-life/x-2819915 QUIT :Ping timeout: 246 seconds < 1760701082 187717 :Lord_of_Life_!~Lord@user/lord-of-life/x-2819915 NICK :Lord_of_Life < 1760701697 724962 :amby!~ambylastn@host-81-178-159-19.as13285.net JOIN #esolangs amby :realname < 1760703265 24675 :int-e!~noone@int-e.eu PRIVMSG #esolangs :`' friday < 1760703267 392767 :HackEso!~h@techne.zem.fi PRIVMSG #esolangs :352) as always in sweden everything goes to a fixed pattern: thursday is queueing at systembolaget to get beer and schnaps, friday is pickled herring, schnaps and dancing the frog dance around the phallos, saturday is dedicated to being hung over \ 510) CakeProphet: mr president, in the best egyptian judicial traditions has now been put off to friday. but i want my money back'. we know it generally deals with major infrastructure projects < 1760703292 63889 :int-e!~noone@int-e.eu PRIVMSG #esolangs :oh, I should've known that #352 would come up again < 1760703321 424129 :int-e!~noone@int-e.eu PRIVMSG #esolangs :`` quote friday | paste < 1760703323 618548 :HackEso!~h@techne.zem.fi PRIVMSG #esolangs :https://hack.esolangs.org/tmp/paste/paste.6670 < 1760706019 907011 :ais523!~ais523@user/ais523 QUIT :Quit: quit < 1760706689 431327 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :ZFC+Not(Con(ZFC)) is a perfectly consistent theory (assuming Con(ZFC)), any model must merely have an "inconsistency proof" as a non-standard natural, this is well known < 1760706764 300791 :int-e!~noone@int-e.eu PRIVMSG #esolangs :I keep wondering what separates a standard model of ZFC from others. < 1760707068 525691 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :short answer is that a standard model contains objects which correspond to the metatheory < 1760707256 913842 :Sgeo!~Sgeo@user/sgeo JOIN #esolangs Sgeo :realname < 1760707274 559009 :int-e!~noone@int-e.eu PRIVMSG #esolangs :Cool, but then we're in the situation where it's meta theories all the way down. < 1760707301 281181 :int-e!~noone@int-e.eu PRIVMSG #esolangs :Now I can delude myself into believing that there's a unique standard model for Peano Arithmetic, but set theory is much richer. < 1760707385 185120 :int-e!~noone@int-e.eu PRIVMSG #esolangs :And ZFC (the first-order axiom schema version) has a countable model... and that's not the standard model... or is it... < 1760707406 444757 :int-e!~noone@int-e.eu PRIVMSG #esolangs :Well, I find it very confusing :) < 1760708131 161864 :sorear!sid184231@id-184231.uxbridge.irccloud.com PRIVMSG #esolangs :model theory in general is infinitary, if you want to work concretely you need to translate whatever into the language of proofs < 1760708421 819469 :int-e!~noone@int-e.eu PRIVMSG #esolangs :Yeah, fortunately the answer to this standard model puzzle is irrelevant to doing math. No impact on the real world either. :) < 1760709645 629913 :sprout!~sprout@84-80-106-227.fixed.kpn.net PRIVMSG #esolangs :them's fighting words < 1760710332 763907 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :int-e: Fortunately, in second-order logic, there's only *the* one unique natural numbers. < 1760710352 487372 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :But yeah, if one doesn't know that then non-standard nats are going to always be spooky. Appropriate for October, at least. < 1760710624 980290 :int-e!~noone@int-e.eu PRIVMSG #esolangs :korvo: Sure, but then you get that natural numbers are unique in each model of set theory, and it's still relative to picking a model of that ;) < 1760710681 59113 :int-e!~noone@int-e.eu PRIVMSG #esolangs :(The fundamental issue will always be this infinite stack of meta-theories.) < 1760710719 479719 :int-e!~noone@int-e.eu PRIVMSG #esolangs :Anyway. It is fun to ponder, but I don't expect any answers. I'll happily leave that to philosophers ;) < 1760710748 884175 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :int-e: Yeah. At the same time, we can imagine that second-order logic, which presupposes those sets, has *enough* subsets of natural numbers. There's some nasty subsets like 0♯ whose existence has implications, but just taking a finite or cofinite set isn't a problem. < 1760712910 506118 :tromp!~textual@2001:1c00:3487:1b00:d983:2af2:5deb:9bbb JOIN #esolangs * :Textual User > 1760712998 413174 PRIVMSG #esolangs :14[[07Turing machine14]]4 10 02https://esolangs.org/w/index.php?diff=166165&oldid=154622 5* 03Corbin 5* (+1270) 10Stub a section on halting. Most of the good stuff's already in [[computable]], but the overview isn't stated elsewhere. < 1760713042 185342 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Not really liking the