> 1752451303 967037 PRIVMSG #esolangs :14[[07User:Pifrited/NameNeeded14]]4 10 02https://esolangs.org/w/index.php?diff=161289&oldid=161268 5* 03Pifrited 5* (+215) 10/* Examples */
> 1752451377 397466 PRIVMSG #esolangs :14[[07User:Pifrited/NameNeeded14]]4 M10 02https://esolangs.org/w/index.php?diff=161290&oldid=161289 5* 03Pifrited 5* (+0) 10
< 1752467248 14438 :Lord_of_Life!~Lord@user/lord-of-life/x-2819915 QUIT :Ping timeout: 265 seconds
< 1752467341 476508 :Lord_of_Life!~Lord@user/lord-of-life/x-2819915 JOIN #esolangs Lord_of_Life :Lord
< 1752468540 203183 :citrons!~citrons@alt.mondecitronne.com QUIT :Remote host closed the connection
> 1752469284 274638 PRIVMSG #esolangs :14[[07User:I am islptng14]]4 10 02https://esolangs.org/w/index.php?diff=161291&oldid=161272 5* 03I am islptng 5* (+46) 10/* Other things */
< 1752475548 393586 :tromp!~textual@2001:1c00:3487:1b00:89d3:7d92:7b20:925 JOIN #esolangs * :Textual User
< 1752477506 877347 :Sgeo!~Sgeo@user/sgeo QUIT :Read error: Connection reset by peer
< 1752478255 552378 :tromp!~textual@2001:1c00:3487:1b00:89d3:7d92:7b20:925 QUIT :Quit: My iMac has gone to sleep. ZZZzzz…
< 1752479424 765243 :tromp!~textual@2001:1c00:3487:1b00:89d3:7d92:7b20:925 JOIN #esolangs * :Textual User
> 1752480794 737317 PRIVMSG #esolangs :14[[07Ku14]]4 M10 02https://esolangs.org/w/index.php?diff=161292&oldid=161282 5* 03Shivani 5* (+0) 10
> 1752481184 570776 PRIVMSG #esolangs :14[[07User:Pifrited/NameNeeded14]]4 M10 02https://esolangs.org/w/index.php?diff=161293&oldid=161290 5* 03Pifrited 5* (+65) 10
< 1752482643 28687 :chomwitt!~alex@2a02:85f:9a3f:9300:42b0:76ff:fe46:a5fd JOIN #esolangs chomwitt :realname
< 1752482654 300790 :tromp!~textual@2001:1c00:3487:1b00:89d3:7d92:7b20:925 QUIT :Quit: My iMac has gone to sleep. ZZZzzz…
> 1752482767 455448 PRIVMSG #esolangs :14[[07User talk:Pifrited/NameNeeded14]]4 10 02https://esolangs.org/w/index.php?diff=161294&oldid=161270 5* 03I am islptng 5* (+152) 10
< 1752486515 532648 :tromp!~textual@2001:1c00:3487:1b00:89d3:7d92:7b20:925 JOIN #esolangs * :Textual User
> 1752487284 128867 PRIVMSG #esolangs :14[[07User talk:Pifrited/NameNeeded14]]4 10 02https://esolangs.org/w/index.php?diff=161295&oldid=161294 5* 03Pifrited 5* (+143) 10
> 1752488610 84751 PRIVMSG #esolangs :14[[07Bobr Kurwa14]]4 10 02https://esolangs.org/w/index.php?diff=161296&oldid=159369 5* 03Bobr123654 5* (+6) 10
< 1752489434 967165 :APic!apic@apic.name PRIVMSG #esolangs :Hi
> 1752491053 262700 PRIVMSG #esolangs :14[[07User:Pifrited/NameNeeded14]]4 10 02https://esolangs.org/w/index.php?diff=161297&oldid=161293 5* 03Pifrited 5* (+661) 10/* Examples */
> 1752491720 798482 PRIVMSG #esolangs :14[[07Piet14]]4 10 02https://esolangs.org/w/index.php?diff=161298&oldid=155900 5* 03B jonas 5* (-51) 10rv https://esolangs.org/w/index.php?title=Piet&diff=prev&oldid=155084 by JHSHernandez-ZBH 12:52, 4 April 2025
> 1752492138 508424 PRIVMSG #esolangs :14[[07User:Pifrited/NameNeeded14]]4 10 02https://esolangs.org/w/index.php?diff=161299&oldid=161297 5* 03Pifrited 5* (+144) 10/* Truth-machine */
> 1752492184 397069 PRIVMSG #esolangs :14[[07User:Pifrited/NameNeeded14]]4 M10 02https://esolangs.org/w/index.php?diff=161300&oldid=161299 5* 03Pifrited 5* (+4) 10/* Truth-machine */
> 1752492272 886892 PRIVMSG #esolangs :14[[07User:Pifrited/NameNeeded14]]4 M10 02https://esolangs.org/w/index.php?diff=161301&oldid=161300 5* 03Pifrited 5* (-22) 10/* Truth-machine */ Reduce
> 1752494048 491051 PRIVMSG #esolangs :14[[07User talk:Pifrited/NameNeeded14]]4 10 02https://esolangs.org/w/index.php?diff=161302&oldid=161295 5* 03I am islptng 5* (+173) 10
> 1752495858 210923 PRIVMSG #esolangs :14[[07User:Pifrited/NameNeeded14]]4 M10 02https://esolangs.org/w/index.php?diff=161303&oldid=161301 5* 03Pifrited 5* (+547) 10
< 1752496592 878088 :amby!~ambylastn@ward-15-b2-v4wan-167229-cust809.vm18.cable.virginm.net JOIN #esolangs * :realname
> 1752496654 166183 PRIVMSG #esolangs :14[[07User:Pifrited/NameNeeded14]]4 10 02https://esolangs.org/w/index.php?diff=161304&oldid=161303 5* 03Pifrited 5* (+24) 10Test
> 1752497175 729306 PRIVMSG #esolangs :14[[07User talk:Pifrited/NameNeeded14]]4 10 02https://esolangs.org/w/index.php?diff=161305&oldid=161302 5* 03Pifrited 5* (+153) 10
> 1752497205 141814 PRIVMSG #esolangs :14[[07User:Pifrited/NameNeeded14]]4 M10 02https://esolangs.org/w/index.php?diff=161306&oldid=161304 5* 03Pifrited 5* (-24) 10
> 1752498684 633468 PRIVMSG #esolangs :14[[07Orthagonal14]]4 10 02https://esolangs.org/w/index.php?diff=161307&oldid=49846 5* 03Krolkrol 5* (+3047) 10
< 1752499443 568263 :tromp!~textual@2001:1c00:3487:1b00:89d3:7d92:7b20:925 QUIT :Quit: My iMac has gone to sleep. ZZZzzz…
> 1752499714 618953 PRIVMSG #esolangs :14[[07CounterClockWise14]]4 10 02https://esolangs.org/w/index.php?diff=161308&oldid=161236 5* 03I am islptng 5* (+294) 10
< 1752500241 562630 :tromp!~textual@2001:1c00:3487:1b00:89d3:7d92:7b20:925 JOIN #esolangs * :Textual User
< 1752501174 974437 :chomwitt!~alex@2a02:85f:9a3f:9300:42b0:76ff:fe46:a5fd QUIT :Remote host closed the connection
< 1752504489 350136 :zzo38!~zzo38@host-24-207-52-143.public.eastlink.ca QUIT :Ping timeout: 276 seconds
< 1752507816 488712 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Do Bubblegum, Malbolge, and other source-encrypted languages have native type theories? I think that the answer is "yes" but I'm open to discussion.
< 1752511795 554497 :tromp!~textual@2001:1c00:3487:1b00:89d3:7d92:7b20:925 QUIT :Quit: My iMac has gone to sleep. ZZZzzz…
< 1752514217 976477 :FreeFull!~freefull@79.186.55.150.ipv4.supernova.orange.pl JOIN #esolangs FreeFull :FreeFull
< 1752514936 123635 :tromp!~textual@2001:1c00:3487:1b00:207a:b700:e4:7b01 JOIN #esolangs * :Textual User
< 1752518661 898116 :ais523!~ais523@user/ais523 JOIN #esolangs ais523 :(this is obviously not my real name)
< 1752518670 302810 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :korvo: I think the answer might depend on the language
< 1752518702 24620 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :e.g. Bubblegum is effectively Python from the type-theory point of view – you can (at least in theory) make the program valid by adding a comment and that has no type-theoretical impact
< 1752518722 283280 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :whereas for Malbolge, the fact that the commands change when executed feels like it might be something that is part of a type theory
< 1752518743 934299 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :in particular, which cycle a command belongs to is considered a very important aspect of Malbolge programming
< 1752518764 156281 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Sure, the native type theory (NTT?) knows what Bubblegum's ints are, because they're equivalent to Python's ints under the encryption. Encryption only makes it hard for us to compute whether programs are equivalent, but it doesn't change whether that equivalence exists.
< 1752518784 467187 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :(but, commands can be overwritten in memory, moving them onto other cycles, and in practice usually are because most of the useful cycles aren't accessible from the source code)
< 1752518807 73832 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :I think Bubblegum is more of a signed programming language than an encrypted programming language
< 1752518833 973227 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :it is comparatively easy to determine whether a Bubblegum program would be interpreted as Python, and if it is, it is exactly equivalent to the Python program with the same source code
< 1752518864 12815 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :but, it is difficult to find the right magic comment to make the interpreter treat it as Python rather than as raw compressed data to output
< 1752518904 384255 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :A Pear Tree is also an interesting example – it's in the same area as Bubblegum, except that the task of finding the correct magic comment actually is computationally tractable
< 1752518966 251568 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :(which was intentional – I've written quite a few A Pear Tree programs, but it would be difficult without having a chosen-prefix-preimage algorithm available)
< 1752519093 229001 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :I don't think A Pear Tree is different from Bubblegum here. I mean, obviously it's got a different topology, but it *has* a topology.
< 1752519121 195251 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :right, they're in the same category of languages, even though the applications are completely different
< 1752519143 706100 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :A Pear Tree is designed to let you specify redundant versions of your program, so that it can still run correctly if some of them are damaged
< 1752519154 559631 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :As usual, But Is It Art? is a bit of a question. Wang tiles have a NTT though, based on the idea that the *set* of Wang tiles has a topology of subsets, so maybe BIIA? also admits something where we consider the set of tiles and its subsets.
< 1752519157 473717 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :(and even to react to the exact nature of the damage, if necessary)
< 1752519196 25327 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :do languages like Deadfish have a native type theory? I'm guessing "yes, but it's degenerate"
< 1752519198 819758 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :ais523: I suppose it's worth remembering that the NTT of a language might have nothing to do with the strategies that we use for encoding simple examples, or even for larger encodings like homomorphisms or compilation schemes.
< 1752519263 72931 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Yeah. I don't know *how* it degenerates offhand, but I can imagine that there are two equivalent Deadfish programs, and that's enough for a non-trivial NTT.
< 1752519264 162647 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :BIIA? feels to me more like a language *backend* than a language itself, from the type-theoretical point of view
< 1752519296 465358 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :you do have a type theory, but certain programming patterns give you a richer type theory
< 1752519330 55443 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Yeah. An NTT will always be dependently-typed, but maybe there aren't any interesting type constructors.
< 1752519374 635126 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :for example, you can imagine a BIAA? program where all the commands are almost-rectangles whose sides are multiples of a particular constant, and you connect them together jigsaw-style by placing protusions on the sides that match recesses on the sides of other almost-rectangles
< 1752519378 968659 :zzo38!~zzo38@host-24-207-52-143.public.eastlink.ca JOIN #esolangs zzo38 :zzo38
< 1752519394 433045 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :and in that case, the program is parametric over the shapes of the protusions
< 1752519394 722873 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :Although NTT usually will at least have Hoare logic. The reason that Wang tiles and BIIA? are weird here is precisely because they don't admit a Hoare logic either.
< 1752519440 865097 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :BIIA? with arbitrary shapes is much harder to reason about
< 1752519471 765584 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :actually, I guess I am thinking about a compiler from Wang tiles to BIIA? – the compilation is clearly very easy but there are multiple equivalent ways to do it
< 1752519499 141108 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :and I think I would want a way to abstract over the difference in details, *but* I am not sure that that abstraction would generalise to arbitrary BIIA? programs
< 1752519595 180394 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :…and now I have an esolang idea: BIIA? but the corners aren't limited to 90° and the sides aren't limited to integers, and a program halts if it is unable to tile the plane
< 1752519645 715125 :joast!~joast@2603:90d8:500:31cf:5e0f:3f4b:1cfe:5060 JOIN #esolangs joast :joast
< 1752519702 702721 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :I suspect this is both a little harder to program in than BIIA? and substantially harder to implement, so there aren't any real advantages other than the aesthetics
< 1752519704 962450 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :but that might be enough
< 1752519757 683295 :ais523!~ais523@user/ais523 PRIVMSG #esolangs :(I'm pretty sure it's at least TC, but am not sure it is computable, even if you require the side lengths and angles to be computable)
< 1752519923 144660 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :I guess that it depends on what a language is. If a language is a collection of texts with some attached semantics, and semantics have some ordering or equivalence, then there's an underlying category or groupoid which leads to NTT.
< 1752519941 156869 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :So escaping that means not having texts, not having semantics, or not having ordering or equivalence.
< 1752520125 235654 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :For Wang tiles, consider a set of tiles that is TC and that also has two different subsets which are TC. Those subsets are non-trivially equivalent, so we get a groupoid. I think this applies to BIIA? as well. I have no idea about your new extension though.
< 1752520193 600829 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :...Wait, the equivalence might not be a bijection, so we get a category. Still works for NTT.
< 1752522127 468151 :ais523!~ais523@user/ais523 QUIT :Quit: quit
< 1752523105 215784 :zzo38!~zzo38@host-24-207-52-143.public.eastlink.ca PRIVMSG #esolangs :I don't know what "native type theory" means
< 1752523253 304916 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :It's a specific construction in category theory that assigns a dependent type theory to programming languages. This blog post is a pretty good introduction: https://golem.ph.utexas.edu/category/2021/02/native_type_theory.html
< 1752523281 455045 :zzo38!~zzo38@host-24-207-52-143.public.eastlink.ca PRIVMSG #esolangs :OK, I will look
< 1752523325 888440 :korvo!~korvo@2604:a880:4:1d0::4d6:d000 PRIVMSG #esolangs :If the original language is a constructive dependently-typed theory already, then it *is* its own native type theory. That's the intuition. For languages like Python, type-like concepts like ints and lists are identifiable, and we can do Hoare logic over them.
< 1752523808 464677 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :ais523: BIIA kind of also lets you encode redundant copies of the program so if one is damaged the program still works and the damaged shapes can't fit anywhere. except this doesn't work if the damage creates a small shape (or a few small shapes) that tile the plane, eg. a one-tile shape, either by adding a new shape or cutting off a small piece of an existing shape.
< 1752525773 282811 :fizzie!irc@selene.zem.fi PRIVMSG #esolangs :Meh, SendGrid is turning off their free tier (which I use for esolangs.org outgoing emails) in two weeks or so. Have to migrate to something else.
< 1752526231 824084 :b_jonas!~x@88.87.242.184 PRIVMSG #esolangs :uh...
> 1752527152 500283 PRIVMSG #esolangs :14[[07User:Hotcrystal0/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=161309&oldid=160767 5* 03Hotcrystal0 5* (+159) 10
< 1752527722 808032 :citrons!~citrons@alt.mondecitronne.com JOIN #esolangs citrons :citrons
> 1752529458 433111 PRIVMSG #esolangs :14[[07Neb's Art14]]4 N10 02https://esolangs.org/w/index.php?oldid=161310 5* 03HecknTarnation 5* (+4366) 10Creation
> 1752529486 86378 PRIVMSG #esolangs :14[[07User:HecknTarnation14]]4 M10 02https://esolangs.org/w/index.php?diff=161311&oldid=139642 5* 03HecknTarnation 5* (+19) 10
> 1752529575 135705 PRIVMSG #esolangs :14[[07Neb's Art14]]4 M10 02https://esolangs.org/w/index.php?diff=161312&oldid=161310 5* 03HecknTarnation 5* (+0) 10/* Resources */
> 1752529743 218532 PRIVMSG #esolangs :14[[07User:Hotcrystal0/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=161313&oldid=161309 5* 03Hotcrystal0 5* (+134) 10
< 1752530909 875433 :fizzie!irc@selene.zem.fi PRIVMSG #esolangs :I used to just run an SMTP server in the old-fashioned way, but it became hard to get emails reliably delivered.
< 1752531338 32269 :tromp!~textual@2001:1c00:3487:1b00:207a:b700:e4:7b01 QUIT :Quit: My iMac has gone to sleep. ZZZzzz…
< 1752531379 339144 :Sgeo!~Sgeo@user/sgeo JOIN #esolangs Sgeo :realname
> 1752531512 438586 PRIVMSG #esolangs :14[[07User:Hotcrystal0/Sandbox14]]4 10 02https://esolangs.org/w/index.php?diff=161314&oldid=161313 5* 03Hotcrystal0 5* (+126) 10
< 1752534831 461928 :^[!~user@user//x-8473491 QUIT :Ping timeout: 276 seconds
> 1752536806 589200 PRIVMSG #esolangs :14[[07Neb's Art14]]4 M10 02https://esolangs.org/w/index.php?diff=161315&oldid=161312 5* 03HecknTarnation 5* (+6) 10/* Instructions */