2026-01-24 - libera.chat:#esolangs

00:11:18 <esolangs> [[Talk:Combinatory logic]] https://esolangs.org/w/index.php?diff=174151&oldid=174150 * Corbin * (+192) /* Is there anything between IJ and complete bases? */ Good question.

01:11:24 <esolangs> [[Execline]] https://esolangs.org/w/index.php?diff=174152&oldid=147774 * Corbin * (+542) Style, references, bluelinks, more words.

01:25:12 <esolangs> [[Vixen]] https://esolangs.org/w/index.php?diff=174153&oldid=170776 * Corbin * (+775) Senpai noticed me! Save a couple quotes which I think are, in sequence, *extremely* funny. Also explain the name more.

01:26:07 <korvo> https://media.bark.lgbt/media_attachments/files/112/019/720/787/034/539/original/40a24e0f8465b9ca.jpg

01:30:26 <ais523> I am still bothered at the overly literal romanisation "senpai" – romanizations of Japanese are mostly intended to allow English speakers to read and pronounce the word more easily, so it should probably be spelled "sempai" which is also valid and much closer to the actual Japanese pronunciation

01:32:13 <ais523> "senpai" would work well if it were being used to type Japanese on an English keyboard, but I don't think that's the usual motivation

01:33:14 <korvo> As usual, I am half-serious and half-joking, right down the middle like a chimeric housecat.

01:34:46 <ais523> I guess Japanese loanwords from English have often diverged quite some way from their initial English pronunciations and even meanings, so the same happening in reverse isn't so surprising

01:35:27 <korvo> Anyway, I guess Vixen is officially a Linux spin. I have successfully called Vixen methods from inside QEMU after using a Vixen method as the /init. I am tempted to ask for [[Category:Linux distributions]].

01:36:55 <Sgeo> I vaguely started reading about Lean and Rocq, there's an interactive "game" for learning Lean.

01:37:18 <korvo> We kind of have a PNW Japanese dialect and accent. Second-gen folks have an l/r split, and the gendered words are heavily disfavored. There's still a fairly strong distinction between the native speakers and the folks like me who have it as third or fourth language.

01:37:35 <Sgeo> Can those proof things use intuitionistic logic? Or only their own builtin one? I kind of think intuitionistic logic is a bit... unintuitive

01:39:11 <korvo> Sgeo: They aren't really designed for implementing logic in logic. It's a longstanding issue with the type-theory approach to proofs. I don't know what Lean's formalism actually is today ("unsound" TBH) but Rocq's using a fairly nice higher-order lambda calculus, Calculus of Constructions.

01:40:08 <korvo> Contrast with e.g. Metamath where there's set.mm using classical logic and ZFC next to iset.mm using intuitionistic logic and IZF. And further down the road they also have quantum foundations. I tried to contribute linear-logic foundations a few years ago, based on a paper of M. Shulman, but couldn't get it to actually work.

01:41:30 <Sgeo> Would learning about Metamath be a good way to learn... about ZFC and ... other stuff?

01:42:41 <korvo> To answer your earlier question, here's how to make Rocq do any logic you want; the example's fully worked to prove Gödel's theorem, but it could be adjusted to write an interpreter or etc. https://www.r6.ca/Goedel/goedel1.html

01:43:48 <korvo> TBH maybe but probably not. Metamath can help with understanding practical foundations of logic, but it's not a teaching tool. Metamath's real power is that it verifies thousands of proofs/second. What set.mm can teach you is how to start with complex numbers before natural numbers.

01:44:20 <ais523> I get frustrated that Rust doesn't appear to be implemented by desugaring everything into a smaller core language, which has lead to a number of soundness bugs

01:45:37 <korvo> Sgeo: Ah, found it. If you want to understand the *structural ideas* underneath ZFC, I really recommend https://arxiv.org/abs/1212.6543 by Leinster. ZFC itself is a specific programming language where the only datatype is sets. It's verbose and nasty. Leinster cleans it all up.

01:45:39 <ais523> (a good example is my answer https://stackoverflow.com/q/79825066 which got it into the Hot Network Questions sidebar, something that is more to do on Stack Overflow than on smaller Stack Exchange sites, although the "this is caused by not implementing as desugaring" is explained only in the comments)

01:47:02 <korvo> ais523: Nice answer. For some reason I can't articulate yet, this feels like the same shape as finalizers in GC'd runtimes.

01:47:25 <korvo> I guess it's the illegal-looking self-extension of a finalizer's effective lifetime via ordinary mutation.

01:47:59 <ais523> I think I tried to seriously use resurrection-within-finalizer as part of a serious Java project once, but can no longer remember the details

01:48:12 <ais523> I do remember that it either didn't work or was unnecessary, possibly both

01:51:26 <korvo> Oh wow. Nope, instead I apparently *never deleted* the relevant objects. Hilarious code from Past Corbin there.

02:09:24 <b_jonas> ais523: what kind of smaller core language are you thinking of? normally I'd think of one that helps compiling to various CPU native codes, but you have to verify that the program typechecks and lifetime checks before you compile to the small core language, because the core language doesn't ensure safety anymore. but I thought most soundness bugs in rust are from confusing the typechecker.

02:10:24 <ais523> as an example, currently in Rust a closure is its own thing that acts sort-of like a struct – I would prefer it if closures were just desugared directly to structs, and then typechecked in that form

02:12:01 <esolangs> [[User talk:RetroPain]] M https://esolangs.org/w/index.php?diff=174154&oldid=174013 * RetroPain * (+5)

02:12:04 <ais523> well-formedness is another good example, instead of being a rule of the type system the compiler could just desugar into stating the well-formedness-implied bounds explicitly and then check those

02:12:14 <esolangs> [[User talk:RetroPain]] M https://esolangs.org/w/index.php?diff=174155&oldid=174154 * RetroPain * (-5) test

02:12:19 <b_jonas> translating closures to structs is probably possible to simplify compilation, though I don't know if it's also possible in a way that it's enough to do typechecking after the transformation

02:12:43 <esolangs> [[User talk:RetroPain]] https://esolangs.org/w/index.php?diff=174156&oldid=174155 * RetroPain * (+100)

02:13:44 <ais523> b_jonas: a &'a T can't exist if T contains a lifetime shorter than 'a

02:13:59 <ais523> like, it can't even be mentioned by the type system or it causes horrible type system bugs

02:14:38 <ais523> this sort-of makes sense because a &'a T is supposed to always contain a valid T for the entire lifetime 'a, which it couldn't if T becomes invalid at some point during 'a

02:15:04 <ais523> but it seems wrong to me that it breaks on even mentioning the type, even if objects of that type are never constructed

02:16:27 <b_jonas> I think part of the reason why rustc doesn't try to desugar constructs to a simpler language is that rustc tries to give very readable error/warning messages, more so than gcc/clang, and desugaring would make that harder because you'd have to resugar to print the error/warning

02:18:15 <b_jonas> I mean the error/warning messages not only try to prove that your code is wrong, they also often try to give a guess of what you may have meant to write

02:18:43 <ais523> but you don't really need to resugar, just look at the corresponding initial code

02:19:39 <b_jonas> yes, but you need to analyze the initial code to guess what the user meant to write

02:21:28 <b_jonas> anyway, maybe some translation could be done, I was just confused because when you say "translate to a smaller language" I mostly think of one that no longer knows about lifetimes and only implements unsafe rust, and even loses some of the type information besides lifetimes so it can do type-unsafe things

02:22:38 <b_jonas> but closures in particular you can probably translate away, also you can probably eliminate the complex pattern language and let-chains and only use simple match statements on the top-level enum constructor

02:28:35 <b_jonas> I still don't know whether you can actually translate rust to a language that has conditional gotos instead of loops. I hope it can be.

03:41:01 <b_jonas> Hooloovoo: yes, but this is about intermediate forms before that

03:42:29 <esolangs> [[Endfield]] N https://esolangs.org/w/index.php?oldid=174157 * Cleverxia * (+1800) Created page with "Endfield is yet another esolang created by [[User:cleverxia]]. It's a brainfuck derivative. The commands are due to the fact that when you pay to the game Endfield, it deduces money from a random account, and you can login on your account on other devices wit cache

03:43:16 <Hooloovoo> I will admit that the last question was basically the only part of the conversation I understood fully

03:43:17 <esolangs> [[User:Cleverxia]] https://esolangs.org/w/index.php?diff=174158&oldid=174087 * Cleverxia * (+43) /* Current Esolangs I've created */

05:43:44 <Sgeo> I don't understand true but not provable. Is the continuum hypothesis a statement that might be true but not provable? I'm vaguely under the impression that there's a way to envision ZFC where CH is true and a way to envision it where it's false. So is that... a different sort of thing from statements which might be true but not provably true?

05:54:28 <korvo> Kind of. CH is *independent*. Like, suppose we have a function f(0) = N, f(n + 1) = f(n) → 2. This is the iterated power set of the natural numbers. (This could be called aleph or bet in some texts, but it's not consistent.)

05:55:57 <korvo> CH says that f(1) = R. Cantor's theorem says N ≠ R, so f(0) ≠ R. But other than that, it turns out that we can construct worlds where f(k) = R for any nonzero k, your choice, made to order. So CH is independent of the usual rules of set theory; it's a free choice to make.

05:57:22 <korvo> Gödel's true-but-unprovable is something different. There's a standard answer and a non-standard answer. Let G be true-but-unprovable; you the human are convinced G is true by construction, but that same construction says ZFC cannot prove G.

05:58:14 <korvo> The standard answer is that G is true, so ZFC + G is a fine theory. Indeed the model of natural numbers we get this way is the same one as before; we have this new true fact G which doesn't contradict ZFC's axioms at all and which we couldn't reach otherwise.

05:58:17 <sorear> CH is provably (in PRA or weaker systems) not provable or disprovable in ZFC. Whether CH is true, false, or objectively meaningless is a philosophical question outside the scope of formal mathematics

05:59:39 <korvo> We can also try ZFC + ~G but it's non-standard, which is how we say "weird" in model theory. ~G means that there *is* a proof of G, somewhere out there in the ether. By tradition, call its Gödel number c. c isn't a finite natural number, but more like a constant for a polynomial ring.

06:00:15 <sorear> (in every set theory text I've seen, beth = iterated power set of the naturals, aleph = iterated cardinal successor of the naturals, beth(1) = R, CH is "aleph(1) also = R")

06:01:38 <sorear> the cardinal successor of a set S is a bit abstract but can be interpreted as the number of order types of at most S elements, so aleph(1) is the set of countable ordinals

06:02:53 <korvo> Sgeo: Sorry if that's kind of an infodump. In short, let CH(k) := f(k) = R, then ZFC + CH(1) and ZFC + CH(2) and ZFC + CH(k) in general and also ZFC + G are good theories that do what you expect, and ZFC + ~G has a non-standard model.

06:04:46 <Sgeo> I tried to wrap my mind around non-standard models, and got so far as to understand that stuff like "a number other than the natural numbers that fits within the Peano axioms" is an example but not the only one

06:05:42 <korvo> sorear: Interestingly, it comes up in category theory, but not for the normal size-issue reasons; it turns out that "all beths exist" is independent of structural set theory. Category theory just doesn't have the big cardinals by default. TBH our foundations can't even distinguish ordinals and cardinals!

06:07:41 <korvo> Sgeo: There's a kind of semiotic/graph approach, and there's also a game-semantics approach. And yeah, I can give another example really easily once we understand either approach for a Gödel model.

06:08:52 <sorear> If you have a model of ZFC you can construct a model of ZFC + CH (e.g. Godel's L) and a model of ZFC + ~CH (e.g. omega(2) Cohen reals). You can recast both of these as interpretations and avoid the problems associated with a model

06:09:11 <korvo> In terms of graphs, we can structure the natural numbers as 0 → 1 → 2 → …, one long chain with one starting point. An object is a model of nats precisely when we can find this chain structure somewhere inside it.

06:10:31 <korvo> The successor axiom says that progressing along this chain is a function. But that's really the only hard rule. So a Gödel model just imagines that there's another chain, … → c -1 → c → c + 1 → … floating along, inaccessible from the initial chain.

06:11:34 <sorear> you usually want the Rosser sentence instead "for every proof of this statement there is a shorter proof of its negation"

06:12:06 <korvo> We can also drop the requirement that successors are injective. So in that case we could have models that start at some side constant c → c + 1 → … → 1 → 2 → … And those are non-standard as well. A model just has to have that initial chain, or "initial segment" in the literature.

06:15:14 <korvo> Sgeo: I guess another important thing is that non-standard models *of arithmetic* and *of set theory* are distinct. I kind of assumed that you were looking at the former, since Gödel, but the latter are relevant to history of CH. Sorry for being confusing if that's the case.

06:15:59 <sorear> there are no computable models of PA + ~G, most of interest that you can say about them starts from Henkin's theorem (all consistent first-order theories have models)

06:16:49 <sorear> this is non-constructive since it involves infinitely iteration of the law of the excluded middle, but definable in the set-theoretic sense since you didn't touch choice

06:19:52 <sorear> "non-standard model of set theory" is not particularly standard terminology. both L and forcing models have externally well-ordered ordinals and satisfy exactly the same arithmetical statements as the metatheory

06:20:10 <korvo> IIRC there's no computable models of PA besides the standard model; this is called "Tenenbaum's theorem" or something like that.

06:23:13 <Sgeo> What does this mean for BB(745), which is apparently... independent of ZFC? It feels like that value should, in some platonic sense, have a single correct value

06:23:49 <Sgeo> Unless there's a non-standard ZFC where turing machines behave weirdly

06:24:58 <sorear> unless you're an ultrafinitist that TM either halts after some finite number of steps or it doesn't, sigma_1 arithmetical sentence

06:24:59 <korvo> It means that there's no valid proof in ZFC that decodes at a high level to `BB(745) = k` for any natural k. For if there were, then we have a program that would search for it s.t. we can derive a contradiction from ZFC's axioms.

06:26:31 <korvo> BB is a well-defined function N → N, ZFC just turns out to be too weak of a theory~

06:27:02 <sorear> finished a proof in HOL last year that there is a turing machine T with 748 states such that T halts iff ZFC is inconsistent

06:27:30 <korvo> I guess that we can connect this to true-but-unprovable. BB is total-but-uncomputable relative to ZFC, also relative to SRP or basically any other large-cardinal theory.

06:28:08 <esolangs> [[User:None1/InDev]] https://esolangs.org/w/index.php?diff=174159&oldid=174131 * None1 * (+123) /* Commands */

06:29:28 <korvo> Sgeo: Oh! If you've seen Gödel's Second Incompleteness, then this is a way to think of that result. Gödel says that no finite collection of axioms can capture all the true statements of arithmetic. The BB function happens to give us a metric for measuring how far a set of axioms goes before it runs out of proof power.

06:31:03 <esolangs> [[User:None1/InDev]] https://esolangs.org/w/index.php?diff=174160&oldid=174159 * None1 * (+139) /* Commands */

06:31:26 <sorear> if T halts in less than k steps, then ZFC is inconsistent with a concrete example. if T does not halt in less than k steps (a delta_0 statement, and provable if true in all systems stronger than Q) and BB(748) = k, then (in ZFC) T does not halt and therefore ZFC proves its own consistency and is inconsistent per Godel

06:42:45 <korvo> sorear: Oh wow, that just clicked for me. Nice! Was that in Lean, Isabelle, or something else?

06:46:43 <ais523> korvo: I think your statement of the continuum hypothesis is wrong – N→2 is known to have the same cardinality as the reals (this is pretty easy to prove), the question is as to whether there's anything with a cardinality between that of N and R

06:48:34 <korvo> ais523: That sounds entirely reasonable. I have yet to actually look anything up and I do often emit plausible-sounding bullshit.

06:52:40 <ais523> hmm, an interesting way to view the busy beaver function is as a map from the size of a false conjecture to the size of the smallest counterexample to it

06:54:01 <ais523> so knowing the values of the busy beaver function would let you prove anything by brute-forcing for counterexamples – but the only way to actually calculate the values in the first place is to check every possible conjecture of a given size and try to prove or disprove it, so trying to use the function for that purpose doesn't help

06:56:47 <ais523> and now I'm thinking about the fact that any prefix of the busy beaver function is theoretically computable just by hardcoding the values, but no program can encode the entire sequence because it will eventually discover a conjecture about its own behaviour

06:57:18 <ais523> well, they're both similarly useful, it's just that for Chaitin's constant the brute-forcing is faster

06:58:14 <ais523> or, hmm, is it even faster? thinking about it, it's probably slower, because you have to run all the other programs too in order to see which ones halt earlier

06:59:31 <ais523> (although Chaitin's constant does have the advantage of working with reasonable-sized numbers rather than Busy Beaver-sized numbers, I don't think that advantage actually helps once you start actually doing the brute-forcing)

07:03:58 <b_jonas> oh yeah, korvo's first formulation was indeed wrong, I didn't even notice

07:05:15 <korvo> My purpose in life is to be wrong, misleading, or straight-up incorrect.

07:07:00 <sorear> if the universe turns out not to be discretizable in meaningful way we can ask if CH corresponds to a meaningful physical question, even if formal mathematics has little to say about it

07:43:04 <esolangs> [[Talk:Polynomix]] https://esolangs.org/w/index.php?diff=174161&oldid=173962 * Yayimhere2(school) * (-2) /* user:Yayimhere's suggestions */

08:11:08 <esolangs> [[Talk:Combinatory logic]] https://esolangs.org/w/index.php?diff=174162&oldid=174151 * Blashyrkh * (+344) /* Is there anything between IJ and complete bases? */ Preliminary simulation results

08:28:45 <esolangs> [[Cammy]] https://esolangs.org/w/index.php?diff=174163&oldid=172438 * Yayimhere2(school) * (+12) Change just "corbin" to "Corbin Simpson", and link to the relevant page, in the infobox.

08:30:22 <esolangs> [[Lye]] https://esolangs.org/w/index.php?diff=174164&oldid=170193 * Yayimhere2(school) * (+3) [[User:Corbin]] -> Corbin Simpson, and link to relevant page(infobox)

08:31:02 <esolangs> [[Monte]] https://esolangs.org/w/index.php?diff=174165&oldid=166467 * Yayimhere2(school) * (+3) [[User:Corbin]] -> Corbin Simpson, link to relevant page in infobox.

08:31:54 <esolangs> [[Zaddy]] https://esolangs.org/w/index.php?diff=174166&oldid=161275 * Yayimhere2(school) * (+12) User:Corbin -> Corbin Simpson, and link to relevant page in infobox.

08:50:46 <esolangs> [[User:Blashyrkh]] https://esolangs.org/w/index.php?diff=174167&oldid=172687 * Blashyrkh * (+149)

09:01:20 <esolangs> [[User:Blashyrkh/Between IJ and SK]] N https://esolangs.org/w/index.php?oldid=174168 * Blashyrkh * (+1460) Created page with "Is there a non-complete system of combinators that includes IJ system as a subset? Equivalent: is there a cancellative combinator X for which K combinator can't be expressed in IJX basis? The opposite question: is it enough to add ''any'' can

09:14:08 <esolangs> [[User talk:Blashyrkh/Between IJ and SK]] N https://esolangs.org/w/index.php?oldid=174169 * Yayimhere2(school) * (+141) Created page with "Can we get the program? --~~~~"

09:26:51 <esolangs> [[Talk:Vixen]] N https://esolangs.org/w/index.php?oldid=174170 * Yayimhere2(school) * (+133) Created page with "exTREMELY cool. --~~~~"

09:29:33 <esolangs> [[User:Yayimhere]] https://esolangs.org/w/index.php?diff=174171&oldid=174008 * Yayimhere2(school) * (+81)

09:30:23 <esolangs> [[User:Yayimhere]] https://esolangs.org/w/index.php?diff=174172&oldid=174171 * Yayimhere2(school) * (-1)

09:30:51 <esolangs> [[User talk:Blashyrkh/Between IJ and SK]] https://esolangs.org/w/index.php?diff=174173&oldid=174169 * Blashyrkh * (+390)

09:37:50 <esolangs> [[Anti-Plushie language DIY]] https://esolangs.org/w/index.php?diff=174174&oldid=169071 * PrySigneToFry * (+79)

09:39:33 <esolangs> [[Anti-Plushie language]] https://esolangs.org/w/index.php?diff=174175&oldid=169075 * Yayimhere2(school) * (+37) /* Commands */

09:40:06 <esolangs> [[Talk:Anti-Plushie language DIY]] https://esolangs.org/w/index.php?diff=174176&oldid=173964 * Yayimhere2(school) * (+141)

09:52:04 <esolangs> [[InterpretMe]] https://esolangs.org/w/index.php?diff=174177&oldid=155389 * Yayimhere2(school) * (+29) /* Lua */ make a see also section, with [[serious]] linked.

09:52:13 <esolangs> [[InterpretMe]] https://esolangs.org/w/index.php?diff=174178&oldid=174177 * Yayimhere2(school) * (+4) /* See also */

09:52:33 <esolangs> [[Serious]] https://esolangs.org/w/index.php?diff=174179&oldid=172629 * Yayimhere2(school) * (+30)

09:55:30 <esolangs> [[Serious]] https://esolangs.org/w/index.php?diff=174180&oldid=174179 * Yayimhere2(school) * (+129)

10:09:39 <esolangs> [[User:Blashyrkh/Between IJ and SK]] https://esolangs.org/w/index.php?diff=174181&oldid=174168 * Blashyrkh * (+61) Link to the program

10:11:04 <esolangs> [[User:Blashyrkh/Between IJ and SK]] M https://esolangs.org/w/index.php?diff=174182&oldid=174181 * Blashyrkh * (+85) More search results

10:15:36 <esolangs> [[User talk:Blashyrkh/Between IJ and SK]] M https://esolangs.org/w/index.php?diff=174183&oldid=174173 * Blashyrkh * (+198) how to build and run

10:37:53 <esolangs> [[User:Blashyrkh/Between IJ and SK]] https://esolangs.org/w/index.php?diff=174184&oldid=174182 * Blashyrkh * (+722) more (and no more) search results

10:41:38 <esolangs> [[User:Blashyrkh/Between IJ and SK]] M https://esolangs.org/w/index.php?diff=174185&oldid=174184 * Blashyrkh * (-4) reword

10:44:48 <esolangs> [[Talk:Combinatory logic]] M https://esolangs.org/w/index.php?diff=174186&oldid=174162 * Blashyrkh * (+49) /* Is there anything between IJ and complete bases? */ link to the page with search results

10:53:20 <esolangs> [[Mezzo]] https://esolangs.org/w/index.php?diff=174187&oldid=174144 * Stegoratops * (+0) /* Calculator */

11:21:05 <esolangs> [[Spam]] https://esolangs.org/w/index.php?diff=174188&oldid=122505 * Cleverxia * (+2025)

11:58:54 <esolangs> [[!!Fuck]] https://esolangs.org/w/index.php?diff=174189&oldid=140485 * Cleverxia * (+2676) /* Examples */

12:00:55 <esolangs> [[Talk:Combinatory logic]] https://esolangs.org/w/index.php?diff=174190&oldid=174186 * Blashyrkh * (+426) /* What's the exact definition of cancellative combinator? */ new section

12:34:14 <esolangs> [[Programming abillities of different esolangs]] M https://esolangs.org/w/index.php?diff=174191&oldid=151623 * Cleverxia * (+5448) this edit is mass language addition, supported by node.js and regex. revert if you thinks this is inappropirate, or you can add my name in the 'formatters' list.

12:37:20 <esolangs> [[Programming abillities of different esolangs]] https://esolangs.org/w/index.php?diff=174192&oldid=174191 * Cleverxia * (-22159) removed the 'needs conversion', since the mass conversion is already done. revert the 2 edits if you think anything isn't appropriate

13:07:18 <esolangs> [[Programming abillities of different esolangs]] M https://esolangs.org/w/index.php?diff=174193&oldid=174192 * 47 * (+72)

13:10:29 <esolangs> [[Programming abillities of different esolangs]] M https://esolangs.org/w/index.php?diff=174194&oldid=174193 * 47 * (-34) oh wait i didn't do anything, oops

13:18:03 <esolangs> [[!frjnrehrbwgyrigbyieurgbyfaerkhbvrwgtr.]] M https://esolangs.org/w/index.php?diff=174195&oldid=173544 * 47 * (-289)

13:18:28 <esolangs> [[!frjnrehrbwgyrigbyieurgbyfaerkhbvrwgtr.]] M https://esolangs.org/w/index.php?diff=174196&oldid=174195 * 47 * (-14) /* Examples */

13:22:44 <esolangs> [[!frjnrehrbwgyrigbyieurgbyfaerkhbvrwgtr.]] M https://esolangs.org/w/index.php?diff=174197&oldid=174196 * 47 * (+18)

14:01:08 <esolangs> [[User:Hotcrystal0/Sandbox]] https://esolangs.org/w/index.php?diff=174198&oldid=174147 * Hotcrystal0 * (+108)

14:12:47 <esolangs> [[User:Blashyrkh/Between IJ and SK]] https://esolangs.org/w/index.php?diff=174199&oldid=174185 * Blashyrkh * (+1294) Beginning of the proof

14:26:39 <esolangs> [[Programming abillities of different esolangs]] https://esolangs.org/w/index.php?diff=174200&oldid=174194 * I am islptng * (+172) add SLet

14:27:20 <esolangs> [[Programming abillities of different esolangs]] M https://esolangs.org/w/index.php?diff=174201&oldid=174200 * I am islptng * (+2) fix

14:43:59 <esolangs> [[User:Blashyrkh/Between IJ and SK]] https://esolangs.org/w/index.php?diff=174202&oldid=174199 * Blashyrkh * (+1123) a little more bit of the proof

14:45:17 <esolangs> [[Pain]] M https://esolangs.org/w/index.php?diff=174203&oldid=173645 * 47 * (-638)

14:46:25 <esolangs> [[Pain]] M https://esolangs.org/w/index.php?diff=174204&oldid=174203 * 47 * (+0)

14:46:57 <esolangs> [[Nope]] https://esolangs.org/w/index.php?diff=174205&oldid=172410 * Yayimhere2(school) * (+6)

15:01:40 <esolangs> [[User:Blashyrkh/Between IJ and SK]] M https://esolangs.org/w/index.php?diff=174206&oldid=174202 * Blashyrkh * (+621)

15:11:16 <esolangs> [[User:Blashyrkh/Between IJ and SK]] https://esolangs.org/w/index.php?diff=174207&oldid=174206 * Blashyrkh * (+61) /* Some ideas for the proof */ More strict definition of case 1 (to satisfy requirements of case 3)

17:46:13 <esolangs> [[Bfppp]] N https://esolangs.org/w/index.php?oldid=174208 * Sourceguy * (+691) Created page with "'''Bfppp''' is an esolang created by [[User:Sourceguy]]. It's an extension of Brainfuck. It contains a standard library, that makes coding in it a bit easier. == Instructions == '''Bfppp supports all Brainfuck instructions, and includes some new ones:''' * # - Commen

17:46:55 <esolangs> [[Bfppp]] https://esolangs.org/w/index.php?diff=174209&oldid=174208 * Sourceguy * (+54)

17:48:31 <esolangs> [[User:Sourceguy]] https://esolangs.org/w/index.php?diff=174210&oldid=136792 * Sourceguy * (+12)

18:33:13 <esolangs> [[!frjnrehrbwgyrigbyieurgbyfaerkhbvrwgtr.]] https://esolangs.org/w/index.php?diff=174211&oldid=174197 * Corbin * (+30) Tag slop. It's important to not let the design credit be reassigned from chatbots to humans.

18:48:00 <esolangs> [[Talk:Eodermdrome]] https://esolangs.org/w/index.php?diff=174212&oldid=59729 * Yayimhere2(school) * (+299) /* Just making sure I understand */ new section

18:52:44 <esolangs> [[Talk:Eodermdrome]] https://esolangs.org/w/index.php?diff=174213&oldid=174212 * Yayimhere2(school) * (+0) /* Just making sure I understand */

18:59:34 <esolangs> [[Talk:Eodermdrome]] https://esolangs.org/w/index.php?diff=174214&oldid=174213 * Yayimhere2(school) * (+238)

19:04:46 <esolangs> [[Set Trickery]] N https://esolangs.org/w/index.php?oldid=174215 * A() * (+515) Created page with "Set Trickery is a set-based programming language that [[User:A()]] made. == Commands == {| class="wikitable" |+ Commands |- ! Command !! Explanation |- | <code>(null) || empty set |- | <code>(set{}) || set |- | <code>(a/.../) || define a as ... |- | <code>[a:b] || add a

19:31:58 <esolangs> [[Not My Type]] N https://esolangs.org/w/index.php?oldid=174216 * Yayimhere2(school) * (+2301) Created page with "'''Not My Type''', named after its lack of actually being a type based language, yet still "claiming" to be, is an esoteric programming language created by [[User:Yayimhere]], based on the <code>N -> (N -> N)</code> type notation. == Definition == Not My

19:32:57 <esolangs> [[Not My Type]] https://esolangs.org/w/index.php?diff=174217&oldid=174216 * Yayimhere2(school) * (-19) /* Definition */

19:34:33 <esolangs> [[Not My Type]] https://esolangs.org/w/index.php?diff=174218&oldid=174217 * Yayimhere2(school) * (+57)

19:37:34 <esolangs> [[Not My Type]] https://esolangs.org/w/index.php?diff=174219&oldid=174218 * Yayimhere2(school) * (+55) /* Example */

19:38:06 <esolangs> [[Not My Type]] https://esolangs.org/w/index.php?diff=174220&oldid=174219 * Yayimhere2(school) * (+1) /* See also */

19:45:04 <esolangs> [[Not My Type]] https://esolangs.org/w/index.php?diff=174221&oldid=174220 * Yayimhere2(school) * (+50) /* Definition */

19:46:08 <esolangs> [[Not My Type]] https://esolangs.org/w/index.php?diff=174222&oldid=174221 * Yayimhere2(school) * (+43) /* Definition */

19:46:28 <esolangs> [[Not My Type]] https://esolangs.org/w/index.php?diff=174223&oldid=174222 * Yayimhere2(school) * (+8) /* Example */

19:57:31 <esolangs> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=174224&oldid=174132 * Rainwave * (+227) /* Introductions */

19:57:39 <esolangs> [[]] https://esolangs.org/w/index.php?diff=174225&oldid=120509 * Yayimhere2(school) * (+0) /* Overview */

20:07:16 <esolangs> [[Talk:]] https://esolangs.org/w/index.php?diff=174226&oldid=82273 * Yayimhere2(school) * (+282) /* turing completeness? */ new section

20:12:05 <esolangs> [[Talk:Eodermdrome]] https://esolangs.org/w/index.php?diff=174227&oldid=174214 * Keymaker * (+212) Graphs.

20:12:35 <esolangs> [[User:Blashyrkh/Between IJ and SK]] https://esolangs.org/w/index.php?diff=174228&oldid=174207 * Blashyrkh * (+213) /* Some ideas for the proof */ The program has found a really tough case

20:13:24 <esolangs> [[User:Yayimhere]] https://esolangs.org/w/index.php?diff=174229&oldid=174172 * Yayimhere2(school) * (-86) /* esolangs */

20:23:25 <esolangs> [[User talk:Blashyrkh/Between IJ and SK]] https://esolangs.org/w/index.php?diff=174230&oldid=174183 * Blashyrkh * (+148) /* Does John Tromp know the answer? */ new section

20:24:03 <esolangs> [[User talk:Blashyrkh/Between IJ and SK]] M https://esolangs.org/w/index.php?diff=174231&oldid=174230 * Blashyrkh * (+91)

20:34:14 <esolangs> [[Esolang:Introduce yourself]] M https://esolangs.org/w/index.php?diff=174232&oldid=174224 * LeCo13 * (+168)

20:34:57 <esolangs> [[SSEG]] N https://esolangs.org/w/index.php?oldid=174233 * LeCo13 * (+1066) Created page with "SEG or SSEG is an programming language written in only 1s and 0s made by laptopcoder11 <small>''(idk how to properly make pages, so pls improve if u can)''</small> instructions: {| class="wikitable" |- ! instruction !! functionality |- | 000n || decrease register-n |- | 0

22:46:25 <esolangs> [[ELBOG]] M https://esolangs.org/w/index.php?diff=174234&oldid=135737 * CPNK * (+100) add xkcd random number, change ref interpreter url

23:05:44 <esolangs> [[Backtick]] https://esolangs.org/w/index.php?diff=174235&oldid=172577 * Splot-dev * (+694) Added library example.

23:08:05 <esolangs> [[Backtick]] M https://esolangs.org/w/index.php?diff=174236&oldid=174235 * Splot-dev * (+12) Fixed wording.

23:09:03 <esolangs> [[Backtick]] M https://esolangs.org/w/index.php?diff=174237&oldid=174236 * Splot-dev * (-1) More wording fixed.

23:09:56 <esolangs> [[Backtick]] M https://esolangs.org/w/index.php?diff=174238&oldid=174237 * Splot-dev * (+29) changed code - added comment to Libraries section code

23:33:42 <Sgeo> https://www.reddit.com/r/math/comments/18gs6cr/unprovability_vs_independence/