00:01:43 <esolangs> [[User:Pifrited/NameNeeded]] https://esolangs.org/w/index.php?diff=161289&oldid=161268 * Pifrited * (+215) /* Examples */
00:02:57 <esolangs> [[User:Pifrited/NameNeeded]] M https://esolangs.org/w/index.php?diff=161290&oldid=161289 * Pifrited * (+0)
04:27:28 -!- Lord_of_Life has quit (Ping timeout: 265 seconds).
04:29:01 -!- Lord_of_Life has joined.
04:49:00 -!- citrons has quit (Remote host closed the connection).
05:01:24 <esolangs> [[User:I am islptng]] https://esolangs.org/w/index.php?diff=161291&oldid=161272 * I am islptng * (+46) /* Other things */
06:45:48 -!- tromp has joined.
07:18:26 -!- Sgeo has quit (Read error: Connection reset by peer).
07:30:55 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
07:50:24 -!- tromp has joined.
08:13:14 <esolangs> [[Ku]] M https://esolangs.org/w/index.php?diff=161292&oldid=161282 * Shivani * (+0)
08:19:44 <esolangs> [[User:Pifrited/NameNeeded]] M https://esolangs.org/w/index.php?diff=161293&oldid=161290 * Pifrited * (+65)
08:44:03 -!- chomwitt has joined.
08:44:14 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
08:46:07 <esolangs> [[User talk:Pifrited/NameNeeded]] https://esolangs.org/w/index.php?diff=161294&oldid=161270 * I am islptng * (+152)
09:48:35 -!- tromp has joined.
10:01:24 <esolangs> [[User talk:Pifrited/NameNeeded]] https://esolangs.org/w/index.php?diff=161295&oldid=161294 * Pifrited * (+143)
10:23:30 <esolangs> [[Bobr Kurwa]] https://esolangs.org/w/index.php?diff=161296&oldid=159369 * Bobr123654 * (+6)
11:04:13 <esolangs> [[User:Pifrited/NameNeeded]] https://esolangs.org/w/index.php?diff=161297&oldid=161293 * Pifrited * (+661) /* Examples */
11:15:20 <esolangs> [[Piet]] https://esolangs.org/w/index.php?diff=161298&oldid=155900 * B jonas * (-51) rv https://esolangs.org/w/index.php?title=Piet&diff=prev&oldid=155084 by JHSHernandez-ZBH 12:52, 4 April 2025
11:22:18 <esolangs> [[User:Pifrited/NameNeeded]] https://esolangs.org/w/index.php?diff=161299&oldid=161297 * Pifrited * (+144) /* Truth-machine */
11:23:04 <esolangs> [[User:Pifrited/NameNeeded]] M https://esolangs.org/w/index.php?diff=161300&oldid=161299 * Pifrited * (+4) /* Truth-machine */
11:24:32 <esolangs> [[User:Pifrited/NameNeeded]] M https://esolangs.org/w/index.php?diff=161301&oldid=161300 * Pifrited * (-22) /* Truth-machine */ Reduce
11:54:08 <esolangs> [[User talk:Pifrited/NameNeeded]] https://esolangs.org/w/index.php?diff=161302&oldid=161295 * I am islptng * (+173)
12:24:18 <esolangs> [[User:Pifrited/NameNeeded]] M https://esolangs.org/w/index.php?diff=161303&oldid=161301 * Pifrited * (+547)
12:36:32 -!- amby has joined.
12:37:34 <esolangs> [[User:Pifrited/NameNeeded]] https://esolangs.org/w/index.php?diff=161304&oldid=161303 * Pifrited * (+24) Test
12:46:15 <esolangs> [[User talk:Pifrited/NameNeeded]] https://esolangs.org/w/index.php?diff=161305&oldid=161302 * Pifrited * (+153)
12:46:45 <esolangs> [[User:Pifrited/NameNeeded]] M https://esolangs.org/w/index.php?diff=161306&oldid=161304 * Pifrited * (-24)
13:11:24 <esolangs> [[Orthagonal]] https://esolangs.org/w/index.php?diff=161307&oldid=49846 * Krolkrol * (+3047)
13:24:03 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
13:28:34 <esolangs> [[CounterClockWise]] https://esolangs.org/w/index.php?diff=161308&oldid=161236 * I am islptng * (+294)
13:37:21 -!- tromp has joined.
13:52:54 -!- chomwitt has quit (Remote host closed the connection).
14:48:09 -!- zzo38 has quit (Ping timeout: 276 seconds).
15:43:36 <korvo> 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.
16:49:55 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
17:30:17 -!- FreeFull has joined.
17:42:16 -!- tromp has joined.
18:44:21 -!- ais523 has joined.
18:44:30 <ais523> korvo: I think the answer might depend on the language
18:45:02 <ais523> 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
18:45:22 <ais523> whereas for Malbolge, the fact that the commands change when executed feels like it might be something that is part of a type theory
18:45:43 <ais523> in particular, which cycle a command belongs to is considered a very important aspect of Malbolge programming
18:46:04 <korvo> 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.
18:46:24 <ais523> (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)
18:46:47 <ais523> I think Bubblegum is more of a signed programming language than an encrypted programming language
18:47:13 <ais523> 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
18:47:44 <ais523> 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
18:48:24 <ais523> 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
18:49:26 <ais523> (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)
18:51:33 <korvo> 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.
18:52:01 <ais523> right, they're in the same category of languages, even though the applications are completely different
18:52:23 <ais523> 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
18:52:34 <korvo> 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.
18:52:37 <ais523> (and even to react to the exact nature of the damage, if necessary)
18:53:16 <ais523> do languages like Deadfish have a native type theory? I'm guessing "yes, but it's degenerate"
18:53:18 <korvo> 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.
18:54:23 <korvo> 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.
18:54:24 <ais523> BIIA? feels to me more like a language *backend* than a language itself, from the type-theoretical point of view
18:54:56 <ais523> you do have a type theory, but certain programming patterns give you a richer type theory
18:55:30 <korvo> Yeah. An NTT will always be dependently-typed, but maybe there aren't any interesting type constructors.
18:56:14 <ais523> 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
18:56:18 -!- zzo38 has joined.
18:56:34 <ais523> and in that case, the program is parametric over the shapes of the protusions
18:56:34 <korvo> 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.
18:57:20 <ais523> BIIA? with arbitrary shapes is much harder to reason about
18:57:51 <ais523> 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
18:58:19 <ais523> 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
18:59:55 <ais523> …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
19:00:45 -!- joast has joined.
19:01:42 <ais523> 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
19:01:44 <ais523> but that might be enough
19:02:37 <ais523> (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)
19:05:23 <korvo> 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.
19:05:41 <korvo> So escaping that means not having texts, not having semantics, or not having ordering or equivalence.
19:08:45 <korvo> 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.
19:09:53 <korvo> ...Wait, the equivalence might not be a bijection, so we get a category. Still works for NTT.
19:42:07 -!- ais523 has quit (Quit: quit).
19:58:25 <zzo38> I don't know what "native type theory" means
20:00:53 <korvo> 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
20:02:05 <korvo> 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.
20:10:08 <b_jonas> 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.
20:42:53 <fizzie> 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.
21:05:52 <esolangs> [[User:Hotcrystal0/Sandbox]] https://esolangs.org/w/index.php?diff=161309&oldid=160767 * Hotcrystal0 * (+159)
21:15:22 -!- citrons has joined.
21:44:18 <esolangs> [[Neb's Art]] N https://esolangs.org/w/index.php?oldid=161310 * HecknTarnation * (+4366) Creation
21:44:46 <esolangs> [[User:HecknTarnation]] M https://esolangs.org/w/index.php?diff=161311&oldid=139642 * HecknTarnation * (+19)
21:46:15 <esolangs> [[Neb's Art]] M https://esolangs.org/w/index.php?diff=161312&oldid=161310 * HecknTarnation * (+0) /* Resources */
21:49:03 <esolangs> [[User:Hotcrystal0/Sandbox]] https://esolangs.org/w/index.php?diff=161313&oldid=161309 * Hotcrystal0 * (+134)
22:08:29 <fizzie> I used to just run an SMTP server in the old-fashioned way, but it became hard to get emails reliably delivered.
22:15:38 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
22:16:19 -!- Sgeo has joined.
22:18:32 <esolangs> [[User:Hotcrystal0/Sandbox]] https://esolangs.org/w/index.php?diff=161314&oldid=161313 * Hotcrystal0 * (+126)
23:13:51 -!- ^[ has quit (Ping timeout: 276 seconds).
23:46:46 <esolangs> [[Neb's Art]] M https://esolangs.org/w/index.php?diff=161315&oldid=161312 * HecknTarnation * (+6) /* Instructions */