00:27:57 <esolangs> [[Godencode]] https://esolangs.org/w/index.php?diff=84400&oldid=84395 * ResU * (+17)
00:46:39 <esolangs> [[Coeus]] https://esolangs.org/w/index.php?diff=84401&oldid=78485 * Kaveh Yousefi * (+150) Added a section Interpreters with a reference to my implementation and changed the category to Implemented.
01:09:36 -!- dbohdan has quit (Read error: Connection reset by peer).
01:10:13 -!- dbohdan has joined.
01:16:10 <esolangs> [[Truth-machine]] https://esolangs.org/w/index.php?diff=84402&oldid=84357 * Plasmath * (+2108)
01:17:09 -!- dbohdan has quit (Excess Flood).
01:17:22 -!- dbohdan has joined.
01:33:39 <esolangs> [[User talk:Ais523]] https://esolangs.org/w/index.php?diff=84403&oldid=83539 * Plasmath * (+400) /* Program too long to add into page */ new section
01:34:54 <esolangs> [[Language list]] M https://esolangs.org/w/index.php?diff=84404&oldid=84385 * Plasmath * (+16) Added [[Godencode]].
01:35:15 -!- lukalot_ has quit (Remote host closed the connection).
01:41:59 -!- xkapastel has quit (Remote host closed the connection).
01:48:16 <esolangs> [[Godencode]] https://esolangs.org/w/index.php?diff=84405&oldid=84400 * Plasmath * (+87) Added an infinite loop. First really simple program.
01:48:43 <esolangs> [[Godencode]] M https://esolangs.org/w/index.php?diff=84406&oldid=84405 * Plasmath * (+1) Forgot the code formatting.
01:49:42 -!- xkapastel has joined.
02:03:58 <zzo38> Why do they use YCoCg rather than YCgCo?
02:10:17 <zzo38> (It seem to me that YCgCo is making a better prediction based on the valid range due to the value of the previous channels)
02:11:45 <esolangs> [[User talk:Plasmath]] N https://esolangs.org/w/index.php?oldid=84407 * Ais523 * (+1030) reply
02:14:30 <esolangs> [[User talk:Plasmath]] https://esolangs.org/w/index.php?diff=84408&oldid=84407 * Ais523 * (+269) what about linking to the language page?
02:41:10 <esolangs> [[User talk:Plasmath]] https://esolangs.org/w/index.php?diff=84409&oldid=84408 * Plasmath * (+124)
02:46:46 <esolangs> [[User talk:Plasmath]] https://esolangs.org/w/index.php?diff=84410&oldid=84409 * Plasmath * (+158)
03:13:54 -!- tromp has joined.
03:14:31 -!- tromp has quit (Client Quit).
03:24:21 <b_jonas> zzo38: you mean like how you order the information in jpeg and such formats? how it would work better if you ordered the channels differently? I don't even know what order it has the channels in. I guess you'd have to test whether it yields a better compression, and of course that may depend on the progressive JPEG scheme. you would have to use an encoder that can take the YUV values directly rather
03:24:28 <b_jonas> than RGB though, and I'm not sure what encoder can do that -- I mean ffmpeg can but its jpeg encoder is also terrible and not configurable so it's not a fair test, maybe libjpeg can but I don't know how
03:25:24 <b_jonas> though the YUV space that JPEG uses isn't quite the same as YCoCg apparently
03:25:37 <b_jonas> I'm confused by so many different linear transformations of color spaces
03:30:57 <b_jonas> I guess you'll have to ask the HAM enthusiasts of esolangs
03:31:36 -!- Lord_of_Life_ has joined.
03:32:49 -!- Lord_of_Life has quit (Ping timeout: 265 seconds).
03:32:50 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
03:47:11 -!- oerjan has quit (Quit: Nite).
04:36:29 <zzo38> b_jonas: I don't mean JPEG, since I think JPEG doesn't take advantage of the order of the channels to make predictions and that stuff. But, it seems to me that the valid range of values for Cg can depend on Y, and the valid range of values for Co can depend on Cg and Y once they are known.
04:36:50 <zzo38> Actually I did make up a picture compression based on this, and it seems to work a bit better than PNG
04:37:27 <zzo38> (and, unlike PNG, does not require guessing things in order to improve the compression)
04:53:58 -!- tromp has joined.
04:55:06 -!- tromp has quit (Client Quit).
05:11:18 <b_jonas> zzo38: oh yeah, it's Huffman compression after that linear transformation on blocks, you'
05:11:53 <b_jonas> re right that it can't take advantage of that kind of thing. I guess I was thinking of PNG, where the deflate step *can* take advantage of correlation between channels
05:14:31 <b_jonas> I should have known that, because I know how JPEG worked, but I didn't realize. oh well.
05:15:21 <b_jonas> but still, if you think something like flipping the order of chroma channels can help, which I doubt, then you might want to experiment with that on more modern image/video compression formats, ones where it could matter
05:15:39 <b_jonas> I doubt that just flipping two channels would help, but still
05:15:49 <b_jonas> I'm not all that good about image compression
05:16:45 <b_jonas> I had some ideas about them and thought about it enough to realize just how difficult the topic is
05:17:54 <zzo38> See the piccomp.c file (SHA-1 hash is c4e5438e358e174cde4b25ecd536d52f59beb702) in TeXnicard
05:19:51 <b_jonas> basically I tried to think of how to design a good image compression algorithm, and I didn't find a way to get the properties that I want, anything I try would either be bad at compression or would be impossible to implement efficiently, and I have also experimented with existing video compression libraries and they're just too good
05:20:03 <zzo38> What properties do you think that you want?
05:20:24 <b_jonas> it shouldn't stop me from thinking of course, but I haven't been able to think of a good enough design yet, so I want to think about it more before I can implement anything
05:23:06 <b_jonas> zzo38: basically the problem is that decoding something variable width like Huffman is hard in a way that takes advantage of the SIMD capabilities of a CPU (or the same of a GPU). you can parallelize decompression and compression by handling individual large chunk of course, and all the other parts, as in color space transforms and DFT or other linear transforms and PNG-like prediction from previous
05:23:12 <b_jonas> value and video compression's testing which neighboring block is the most similar or even estimating the motion delta more efficiently than trying every possible delta, those can be done in SIMD
05:23:40 <b_jonas> but for the variable bit size huffman-like compression in the end (it doesn't necessarily need to be huffman, could be arithmetic coding) you have to iterate through individual values in series
05:23:53 <zzo38> I think what PNG does compressing the filter types together with the pixel data is a bad idea; it would be better to be separate
05:24:44 <b_jonas> and if you want something that avoids that, better predicting how much to shift the input data or have a fixed width encoding, that is possible, but then you probably have to rearrange the output pixels in an unpredictable order which is even worse, or do some other intersting thing,
05:24:55 <b_jonas> and I think it's probably possible to avoid this trap, but I couldn't yet think of a good way,
05:25:15 <b_jonas> so I should read up if any existing algorithm does that and still manage to do not terrible compression
05:26:05 <b_jonas> and also think about how it could be done
05:26:36 <b_jonas> because that's what I'd like to see form an algorithm, at least for *decompression*, it could be slower for compression perhaps, though it's also worth to have other compression methods that are also fast to encode
05:29:56 <b_jonas> there is some balance between slower compression as a price for slightly smaller encoded form while keeping the same quality and decompression time, and a more important tradeoff of slower compression and decompression and much larger encoded size for better quality, and good image/video encodings already offer both tradeoffs as a somewhat tunable parameter
05:30:45 <b_jonas> though there is something odd here now that I think of it
06:15:50 <esolangs> [[Column]] M https://esolangs.org/w/index.php?diff=84411&oldid=84366 * Dominicentek * (-2) /* Truth Machine */
08:07:39 -!- hendursa1 has joined.
08:10:34 -!- hendursaga has quit (Ping timeout: 252 seconds).
08:14:12 -!- tromp has joined.
08:15:49 -!- imode has quit (Ping timeout: 272 seconds).
08:30:38 <esolangs> [[Column]] M https://esolangs.org/w/index.php?diff=84412&oldid=84411 * Dominicentek * (+12) /* Truth Machine */
08:48:52 -!- tech_exorcist has joined.
09:05:34 <esolangs> [[Column]] M https://esolangs.org/w/index.php?diff=84413&oldid=84412 * Dominicentek * (+17) /* Fizz Buzz */
09:20:47 -!- sweatsuit has joined.
09:20:48 -!- sweatsuit has quit (K-Lined).
09:27:57 -!- dutch has quit (Quit: WeeChat 3.1).
09:31:30 <nakilon> this is function k7*x**7+k6*x**6+k5*x**5+k4*x**4+k3*x**3+k2*x**2+k1*x+k0 and this should be its derivative, right? k7*x**6+k6*x**5+k5*x**4+k4*x**3+k3*x**2+k2*x+k1
09:33:05 <nakilon> but the bottom line doesn't look like derivative of upper one https://i.imgur.com/Pljjzyq.png
09:33:24 <nakilon> it doesn't get above 0 in the middle
09:33:45 -!- Sgeo has quit (Read error: Connection reset by peer).
09:34:10 <nakilon> k0..k7 = [86.37483858758613, -4.3258409149187855, 0.13119312931328275, -0.0022258811427750126, 2.156489053721058e-05, -1.1221319014114155e-07, 2.8163872939164175e-10, -2.530165279150212e-13]
09:36:11 <nakilon> oh no, forgot to multiply by 7, 6, ...
10:00:21 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
10:05:11 <nakilon> b_jonas I've got another example https://i.imgur.com/BlsjZrI.png -- problem here is that they use several different captcha generators and this one doesn't rotate but skews the letters
10:08:21 -!- tromp has joined.
10:12:02 <b_jonas> nakilon: yeah, that can help with the captchas
10:12:38 <myname> uhm, the derivative of k7*x^7 isn't k7*x^6 but 7*k7^6
10:13:08 <myname> same issue with each other part of the sum except the last because x^1 will get a factor of 1
10:13:34 <myname> also, bit surprise, captchas are made to be hard to read
10:15:34 <esolangs> [[Special:Log/move]] move * Ultlang * moved [[Delta Salein Ao]] to [[Delta Salein ]]: the actual name
10:15:52 <nakilon> this one is skewed too, not rotated https://i.imgur.com/dVMMdkT.png
10:16:22 <esolangs> [[Delta Salein ]] M https://esolangs.org/w/index.php?diff=84416&oldid=84414 * Ultlang * (+5)
10:17:30 <nakilon> gotta somehow differentiate them to switch the way of chosing the closest line dot -- using "min x1-x2" instead of "min hypot x1-x2, y1-y2"
10:18:46 <nakilon> or just try both ways until I see which one makes better results on the OCR stage
10:24:32 -!- riv has quit (Quit: Leaving).
10:27:26 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
10:28:45 -!- tromp has joined.
10:35:25 <esolangs> [[What's the dog doin?]] https://esolangs.org/w/index.php?diff=84417&oldid=84389 * GreenThePear * (+827) Revamped the commands, all [x] input will be used as an index + fixing some mistakes
10:53:05 -!- riv has joined.
10:55:37 -!- lambdabot has quit (Quit: brb).
10:56:48 -!- lambdabot has joined.
11:18:24 <b_jonas> myname: yes, and nakilon corrected himself about the derivatives a few lines later, and this time I wasn't hasty enough to reply before reading that
11:22:42 <esolangs> [[Column]] https://esolangs.org/w/index.php?diff=84418&oldid=84413 * Dominicentek * (+137)
11:26:05 -!- arseniiv has joined.
11:29:06 <esolangs> [[NumberPankackes]] N https://esolangs.org/w/index.php?oldid=84419 * TinyGuy32 * (+1110) Created page with "==NumberPankackes== NumberPankackes is a stack-based esoteric programing language what a stck is: https://esolangs.org/wiki/Stack ==Commands== 1X: pushes X to the st..."
11:29:44 <esolangs> [[User:TinyGuy32]] https://esolangs.org/w/index.php?diff=84420&oldid=84394 * TinyGuy32 * (-829) Blanked the page
11:30:08 <riv> is there a tool that lets me easily cut a picture from an image out/remove background
11:30:17 <riv> GIMPs 'intelligent scissors' aren't that great for it
11:30:48 <riv> I feel like with modern stuff.. it should be possible to just draw a rough outline and get a perfect cutout
11:34:54 <esolangs> [[Language list]] https://esolangs.org/w/index.php?diff=84421&oldid=84404 * TinyGuy32 * (+44)
11:39:10 <esolangs> [[NumberPankackes]] https://esolangs.org/w/index.php?diff=84422&oldid=84419 * TinyGuy32 * (+2)
11:39:23 <b_jonas> riv: it really depends on the image, but try ones that require both a positive and negative sample, that is, points marked strictly inside and strictly outside the object, rather then a rough outline. try (1) GIMP's new foreground select tool, and (2) the GMIC QT gimp plugin's colorizer tools, which are intended to color black and white photos and black and white line art respectively (that's two
11:39:29 <b_jonas> separate tools) based on another image with sample points of color in the objects, but you can ask them for the masks of which colors go exactly where and use that to get a selection mask that you use for something other than selecting an object
11:39:47 <b_jonas> they aren't perfect, but I think they work better than GIMP intelligent scissors
11:40:19 <b_jonas> http://gmic.eu/ to download the G'MIC QT Gimp plugin on windows; install from distro on debian
11:40:49 <b_jonas> note that Gimp has a decent ABI so the same plugin compiled once can be reused for different minor versions of GIMP
11:41:56 <b_jonas> which means you can install G'MIC QT from debian and it will work for a newer version of Gimp that you install from source, as I learned
11:42:21 <b_jonas> that was back when Gimp 2 wasn't yet in debian and I really really wanted Gimp 2 so I installed from source
11:42:33 <b_jonas> now Gimp 2 is in debian stable, and I love that
11:44:29 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
11:45:31 -!- tromp has joined.
12:01:49 -!- tech_exorcist has quit (Quit: tech_exorcist).
12:02:44 -!- tech_exorcist has joined.
12:08:07 <nakilon> now the correctness is limited by how well I apply dilations to make skeletonization go well https://i.imgur.com/ckuQeDp.png
12:08:50 -!- freon has joined.
12:09:05 -!- freon has quit (Write error: Broken pipe).
12:09:11 <nakilon> riv there was online service
12:09:14 <b_jonas> nakilon: yes, and that part is hard
12:09:42 <nakilon> this or maybe it's a clone https://www.remove.bg/ru
12:11:59 -!- freon has joined.
12:14:22 <nakilon> https://i.imgur.com/Ux0aQTH.png
12:16:18 <nakilon> I actually could apply the whole process twice but pixels are rotting
12:16:43 <esolangs> <LKoen> are you trying to teach bot to cheat at captchas?
12:17:21 <nakilon> yeah, script that would send me new vacancies from local job search site
12:17:44 <esolangs> <LKoen> note that there was a fun trick at some point where captchas consisted in two words; the first word was meant to tell whether the user was human or not; the second word was much easier to decipher and actually came from scanned books
12:18:06 <esolangs> <LKoen> and in two months they had digitalized an entire library without optical recognition software
12:18:24 <nakilon> yeah I guess that was recaptcha
12:18:43 <nakilon> now they are teaching self-driving cars
12:21:49 <b_jonas> nakilon: and Google Maps to read house numbers from blurred photos, surely you noticed those captchas
12:22:40 <nakilon> blurred or just photos taken from the distance by self-driven cars to teach them navigate?
12:23:30 <esolangs> <LKoen> I don't remember house numbers
12:24:30 <b_jonas> nakilon: not deliberately blurred, just taken from a distance either by the same cars that Google Maps uses to make street view, or more likely by the airplane cameras that they used to make the incredibly high resolution "satellite view" from five different camera directions that isn't actually from satellites
12:25:02 <nakilon> didn't know about airplanes
12:25:14 <b_jonas> as in, satellite view _is_ from satellites in most areas of the map, but in those places it's also low resolution and only has one camera direction
12:25:39 <b_jonas> so in more populated places that most people view on the map, they used airplane cameras, which can give much higher quality
12:25:46 <nakilon> that would explain how they made all the trees and buildings 3d in there
12:25:51 <b_jonas> just because they're closer
12:26:33 <b_jonas> nakilon: well that's only part of it, part of the 3D buildings are modeled from their street view photos and from random location-tagged photos from the internet corellated by really clever software, the same way as we model 3d objects from 2d photos except they do it better
12:27:27 <b_jonas> and of course some of this is just speculation because they don't tell all the details about how they got every image, they only tell when that was a requirement to buy a license of pictures that other people made not specifically for them
12:40:34 <esolangs> [[NumberPankackes]] M https://esolangs.org/w/index.php?diff=84423&oldid=84422 * PythonshellDebugwindow * (-45) Link to page directly
12:41:10 <esolangs> [[Language list]] M https://esolangs.org/w/index.php?diff=84424&oldid=84421 * PythonshellDebugwindow * (-22) /* Non-alphabetic */ Remove duplicate
12:42:19 <nakilon> at first they were croudsourcing
12:42:38 <nakilon> it was called Warehouse 3d and people could make models of things in Sketchup
12:42:54 <nakilon> Sketchup was freeware and a great fun
12:44:02 <esolangs> [[What Mains Numbers?]] M https://esolangs.org/w/index.php?diff=84425&oldid=64983 * PythonshellDebugwindow * (+35) /* Implementations */ Cat
12:44:08 <nakilon> so I made models for 2-3 buildings in my town, uploaded and they were in Google Earth since then; but now I can't even find them on their website, idk
12:44:41 <nakilon> you could create collections and become moderator of them, similar to how people build wikipedia
12:45:21 <esolangs> [[User:Soundandfury/ECLAIR]] M https://esolangs.org/w/index.php?diff=84426&oldid=33340 * PythonshellDebugwindow * (+13) /* Implementation */ Deadlink
12:46:48 -!- leah2 has quit (Remote host closed the connection).
12:47:12 -!- leah2 has joined.
13:05:48 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
13:08:00 -!- tromp has joined.
13:13:46 -!- hendursa1 has quit (Quit: hendursa1).
13:15:13 -!- hendursaga has joined.
13:18:52 <esolangs> [[Column]] M https://esolangs.org/w/index.php?diff=84427&oldid=84418 * Dominicentek * (-42) /* Interpreter */
13:19:17 <esolangs> [[FolderCode]] M https://esolangs.org/w/index.php?diff=84428&oldid=84361 * Dominicentek * (-41) /* Development Kit */
13:20:50 <esolangs> [[User:Plasmath]] https://esolangs.org/w/index.php?diff=84429&oldid=84393 * Plasmath * (-66) Added [[Godencode]].
13:29:50 <esolangs> [[Hello world program in esoteric languages]] M https://esolangs.org/w/index.php?diff=84430&oldid=83967 * Plasmath * (+20) I'm trying to add Godencode, but it hasn't been letting me. Making it a 2-step process might work?
13:34:24 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
13:35:38 <esolangs> [[Hello world program in esoteric languages]] https://esolangs.org/w/index.php?diff=84431&oldid=84430 * Plasmath * (+47)
13:42:32 -!- FreeFull has joined.
13:47:10 -!- FreeFull has quit (Client Quit).
13:47:55 -!- tiggilyboo has joined.
14:03:45 <esolangs> [[Cheese]] M https://esolangs.org/w/index.php?diff=84432&oldid=83055 * Sanscicondos * (+49)
14:04:09 <esolangs> [[Cheese]] https://esolangs.org/w/index.php?diff=84433&oldid=84432 * Sanscicondos * (+13) Added Version 1.3.5 to Github
14:11:01 -!- tromp has joined.
14:35:20 -!- tiggilyboo has quit (Quit: tiggilyboo).
14:48:52 <esolangs> [[Special:Log/newusers]] create * Kermek * New user account
14:55:02 <esolangs> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=84434&oldid=84388 * Kermek * (+407)
14:55:53 <esolangs> [[Esolang:Introduce yourself]] M https://esolangs.org/w/index.php?diff=84435&oldid=84434 * Kermek * (-76)
14:56:22 <esolangs> [[Esolang:Introduce yourself]] M https://esolangs.org/w/index.php?diff=84436&oldid=84435 * Kermek * (-6)
15:49:30 <nakilon> made the second pass https://i.imgur.com/Jq2LUCj.png
15:57:49 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
15:59:01 <esolangs> [[Dick]] M https://esolangs.org/w/index.php?diff=84437&oldid=79507 * Cybertelx * (+15) Added LongDick language
15:59:22 -!- tromp has joined.
16:12:05 -!- arseniiv has quit (Ping timeout: 272 seconds).
16:13:27 <esolangs> [[LongDick]] M https://esolangs.org/w/index.php?diff=84438&oldid=83816 * Cybertelx * (+19) link me
16:18:58 -!- Sgeo has joined.
16:30:37 -!- craigo has joined.
16:33:12 <esolangs> [[VBF]] N https://esolangs.org/w/index.php?oldid=84439 * VilgotanL * (+2464) created the page
16:34:20 <esolangs> [[VBF]] M https://esolangs.org/w/index.php?diff=84440&oldid=84439 * VilgotanL * (+15) add "and transpiler" to implementation link
16:40:16 <esolangs> [[For The Worthy]] N https://esolangs.org/w/index.php?oldid=84441 * Kermek * (+5730) Created page with "'''For The Worthy''' is an esolang witch only interprets the '1' and '0' characters, thus enabling programmers to reach their final hackerman form. ==Language Overview== ===In..."
16:41:59 <esolangs> <orbitaldecay72> Greetings all. I have a quick question. Is the sort of completeness that Godel talks about equivalent to TC under the Curry-Howard correspondence?
16:44:22 <esolangs> [[Language list]] M https://esolangs.org/w/index.php?diff=84442&oldid=84424 * Kermek * (+21)
16:45:02 <esolangs> <orbitaldecay72> And, if so, is it fair to say that one way to describe the split between computer science and mathematics is in how each field responds to Godel's incompleteness theorem? i.e. mathematicians err on the side of consistency while computer scientists err on the side of completeness?
16:45:33 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
16:49:11 <riv> Godels completeness theorem states that in a first order logic, if a formula is true in all models it is provable
16:49:20 -!- arseniiv has joined.
16:50:05 <riv> Godels incompleteness theorem states that arithmetic (and extensions) contain statements that are neither provable or disprovable
16:51:37 <riv> the halting problem gives an explicit example of a problem that cannot be solved by a turing machine
16:51:53 <esolangs> [[User:VilgotanL]] M https://esolangs.org/w/index.php?diff=84443&oldid=83804 * VilgotanL * (+10) add vbf to language list
16:52:14 <esolangs> <orbitaldecay72> Right, and under the Curry-Howard correspondence, a type system is in some sense equivalent to a Hilbert style deductive system in logic. If a no non-normalizing expression is well typed, then the corresponding logic is consistent, right?
16:52:47 <riv> Curry-Howard correspondence equates proofs and programs
16:53:25 <esolangs> <orbitaldecay72> Yes, and formulas as type definitions, among other things, right?
16:53:34 <riv> generally consistency of a typed lambda calculus based logic is proven by showing (A) strong normalization (B) False does not have a normal form - this implies consistency as inconsistency would let you prove False
16:53:55 <Corbin> orbitaldecay72: If you want the short answer, then yes, by Lawvere's fixed-point theorem: http://tac.mta.ca/tac/reprints/articles/15/tr15.pdf
16:54:26 <esolangs> <orbitaldecay72> Yeah, looking for the short answer to test my intuition. Thanks for the link.
16:54:29 <esolangs> <orbitaldecay72> Appreciate you both.
16:54:30 <Corbin> This is a very abstract category-theoretic statement. It can be specialized to get Gödel's Incompleteness, and also to get Turing's Halting.
16:55:03 <esolangs> <orbitaldecay72> Looks like I need to learn category theory :)
16:55:46 <riv> The completeness that Godel talks about is not the same as turing completeness
16:56:04 <riv> the fact that there are problems a turing machine can't solve is a type of incompleteness
16:56:23 <Corbin> I think that there were many different reactions to our discovery of computability theory. I don't think it's reasonable to cleave computer science from maths; computer science is the study of algorithms and data structures, which is a special case of studying abstraca.
16:56:28 <riv> turing completeness <- may be better referred to as turing equivalence
16:57:17 <Corbin> Oh, I misread the original question, sorry.
16:57:54 <Corbin> Gödel's Completeness is quite different from Gödel's Incompleteness! I don't know how the former relates to Turing's work, sorry.
16:58:13 <esolangs> <orbitaldecay72> Okay, so in the Curry-Howard sense the halting problem corresponds to some theorem that can neither be proven nor disproven?
16:58:16 <esolangs> <orbitaldecay72> Np, thanks Corbin
16:58:59 <esolangs> <orbitaldecay72> Sorry for my vagueness
16:59:06 <esolangs> <orbitaldecay72> Still learning
16:59:06 <riv> https://www.andrew.cmu.edu/user/avigad/Teaching/halting.pdf there is a direct proof here of godels first incompleteness theorem using the halting problem as the key element, rather than godels original proof which used a self referential formula as the key element
16:59:25 <esolangs> <orbitaldecay72> riv: beautiful, this is exactly what I was looking for
16:59:32 <riv> > in the Curry-Howard sense the halting problem corresponds to some theorem that can neither be proven nor disproven?
16:59:34 <lambdabot> <hint>:1:1: error: parse error on input ‘in’
16:59:45 <esolangs> [[Language list]] M https://esolangs.org/w/index.php?diff=84444&oldid=84442 * VilgotanL * (+67) add my newest 5 languages
16:59:49 <riv> no, turing machines aren't a typed lambda calculi - so you cannot apply Curry-Howard here
17:00:37 <esolangs> <orbitaldecay72> yeah, I get that, but typed lambda calculi are of course in some sense equivalent to turing machines, just wondering if it makes sense theoretically
17:00:54 <riv> a typed lambda calculus must not be turing equivalent
17:00:57 <esolangs> <orbitaldecay72> or rather, lambda calculi in general are in some sense equivalent to turing machines
17:01:10 <riv> the strong normalization condition says that every algorithm terminates in a finite number of steps
17:01:11 <esolangs> <orbitaldecay72> I understand that simply typed lambda calculus is not tc
17:01:23 <riv> neither is dependently typed, like Coq for example
17:01:37 <riv> this is what enables a consistency proof to be done
17:01:42 <Corbin> riv: Note that Curry-Howard-Lambek still applies, and typed lambda calculi each give a Cartesian closed category for a model, where we can try to apply Lawvere's fixed-point theorem.
17:02:43 <Corbin> But yeah, generally when it *does* apply, there's enough data for a Turing category, where there's an object representing all of the untyped terms.
17:02:58 -!- tromp has joined.
17:03:31 <riv> the untyped lambda calculus is turing equivalent, but it doesn't have types that you can interpret as logical formulae - so no Curry-Howard bridge there
17:03:35 <Corbin> There's nice tables at https://ncatlab.org/nlab/show/computational+trilogy which are recently redone and looking nice.
17:04:57 <esolangs> <orbitaldecay72> Okay, so, another related question, when Godel talks about incompleteness, is this in some sense equivalent to sub tc? Re: what Corbin was mentioning.
17:05:27 <Corbin> Turing showed that there's a computer program which, if given a program that could solve Halting, creates a contradiction.
17:06:34 <esolangs> <orbitaldecay72> That is my understanding of how the halting problem is proven to be uncomputable
17:06:37 <Corbin> Let "Truth" be the question of whether a formula in arithmetic is true. Gödel showed that there's a proof which, if given a proof that could solve Truth, creates a contradiction.
17:07:09 <Corbin> (Technically Tarski showed this, and similarly we can't mention Turing without the far-more-useful Rice's Theorem; there's too many people to remember~)
17:07:30 <esolangs> <orbitaldecay72> Of course, we all stand on the shoulders of history :)
17:08:50 <riv> What is the connection between Tarski's undefinability of truth and Godels incompleteness?
17:09:10 <riv> > The undefinability theorem is conventionally attributed to Alfred Tarski. Gödel also discovered the undefinability theorem in 1930, while proving his incompleteness theorems published in 1931, and well before the 1933 publication of Tarski's work
17:09:11 <lambdabot> <hint>:1:124: error: parse error on input ‘in’
17:09:13 <riv> oh that is funny I didn't know that
17:12:06 <riv> it doesn't seem to imply godels incompleteness
17:15:30 <Corbin> BTW, https://www.logicmatters.net/resources/pdfs/godelbook/GodelBookLM.pdf is quite good, for anybody wanting to understand all that Gödelian stuff. I had to take it slow, because the details are extremely nuanced.
17:16:30 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
17:17:19 -!- craigo has quit (Quit: Leaving).
17:18:15 <Corbin> If you just want to see how category theorists might apply Lawvere's work to simplify thinking about all of this, then https://arxiv.org/pdf/math/0305282.pdf is so good.
17:27:56 -!- tromp has joined.
17:29:17 <esolangs> [[What's the dog doin?]] https://esolangs.org/w/index.php?diff=84445&oldid=84417 * GreenThePear * (+47) Clarifications and fixes about the number system, plus other polishing
17:31:35 <riv> https://arxiv.org/pdf/math/0305282.pdf <- this is really cool!
17:35:26 <esolangs> [[Godencode]] M https://esolangs.org/w/index.php?diff=84446&oldid=84406 * Plasmath * (+124) Forgot one small part of if command.
17:36:21 <riv> The Lob's Paradox one is a bit jarring
17:42:31 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
17:54:36 -!- tromp has joined.
17:55:33 <esolangs> [[Godencode]] M https://esolangs.org/w/index.php?diff=84447&oldid=84446 * Plasmath * (-3) Made another mistake in the description.
18:05:16 <esolangs> [[Godencode]] M https://esolangs.org/w/index.php?diff=84448&oldid=84447 * Plasmath * (+16) I think I finally worded this in a good way.
18:11:32 <esolangs> <orbitaldecay72> Corbin: I'm thinking more about my comments on the distinction between computer science and mathematics. Most of my experience is as a software engineer. My education is in math, but I don't know a lot about proof theory. The thing I noticed is that, AFAIK, a program which does not halt corresponds to a proof of a contradiction in mathematics by
18:11:33 <esolangs> <orbitaldecay72> Curry-Howard. In programming, we use languages that permit infinite loops, but in mathematics we don't use axiom systems that allow proving contradictions.
18:12:02 <esolangs> <orbitaldecay72> On the surface, this makes sense because in classical logic if we permit a contradiction as a theorem, then everything entails. But in paraconsistent logics this is not true.
18:12:23 <esolangs> <orbitaldecay72> As paraconsistent logics explicitly reject the principle of explosion.
18:13:32 <esolangs> <orbitaldecay72> So, why don't mathematicians use paraconsistent logics to permit a small class of contradictions as theorems but software engineers use languages that permit infinite loops?
18:13:49 <esolangs> [[Godencode]] https://esolangs.org/w/index.php?diff=84449&oldid=84448 * Plasmath * (+31) Forgot yet another thing about this command. This is it though. I've made sure.
18:13:49 <esolangs> <orbitaldecay72> Does this make sense, or am I way off?
18:16:23 <esolangs> <orbitaldecay72> I recognize that what I'm proposing is a totally reformulation of how math is done, but just wondering in the spirit of intellectual inquiry
18:17:29 <Corbin> Sure, and the philosophy of why logic is even a good idea is historically important. Frege and Quine had strong but inscrutable opinions on this sort of thing.
18:18:54 <myname> forbidding infinite loops would need you to solve the halting problem, doesn't it?
18:18:55 <esolangs> [[Meta Memes]] M https://esolangs.org/w/index.php?diff=84450&oldid=72253 * Caenbe * (+9) Stubbify
18:19:02 <esolangs> <orbitaldecay72> Okay, glad I'm making sense. I recently learned about paraconsistent logics and dialetheism and immediately sensed a correlation between what those philosophies are advocating and what I do as a software engineer.
18:19:05 <myname> doesn't sound like an easy task for me
18:19:16 <esolangs> <orbitaldecay72> myname: nah, just make your language sub turing
18:19:25 <Corbin> There is an old question: Shouldn't contradictions be relevant to the proofs which use them? If I prove that the sky is simultaneously blue and not-blue, does that make 1=2? If so, *how*?
18:19:39 <esolangs> [[Godencode]] https://esolangs.org/w/index.php?diff=84451&oldid=84449 * Plasmath * (+0) My documentation was hard to read.
18:19:40 <myname> great, have a language that probably cannot do the task you are trying to solve
18:20:30 <Corbin> Ah, sure. Note that a proper dialethist cannot refute a trivialist, who claims that all things are true. In particular, a dialethist cannot prove to them that anything is false; the law of non-contradiction is a missing logical lever they'd need.
18:20:54 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
18:21:23 <esolangs> <orbitaldecay72> Corbin: Yeah, of course. There are definitely philosophical issues with dialetheism too, I just noticed that philosophically it was closer to what I was doing than classic logic was.
18:21:24 <Corbin> myname: Most GPU programs are not Turing-complete. Instead, a Turing-complete CPU program repeatedly takes bounded steps by submitting bounded programs to the GPU.
18:22:09 <myname> sure, you can have arbitrary many sub-tc sub-tasks, but you want to have a tc system at some point or another
18:22:12 <esolangs> <orbitaldecay72> i.e. by using a language that allows for infinite loops I'm implicity rejecting non-contradiction
18:22:34 <Corbin> orbitaldecay72: I'm looking for a good reference, but a simple slogan is "there's no type of non-halting programs", along myname's lines. This means that it's not possible to use Curry-Howard to try to construct a family of usable contraditions.
18:23:35 <myname> also, at least in terms of semantics, an infinite loop is considered to have no semantical meaning. it's just one of the points where theory and practice diverge
18:23:36 <Corbin> In general, computers are constructive and effective, so while we don't have LEM or Choice, we do still have intuitionistic type theory, which is plenty powerful.
18:23:37 <esolangs> <orbitaldecay72> this is where I don't know enough about formal type theory to recognize what is a limitation of classical logic, and what is a limitation of type theory
18:23:47 <myname> imperative programming makes things hard
18:24:20 <Corbin> orbitaldecay72: Lucky 10000: https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4/S0273-0979-2016-01556-4.pdf
18:25:46 <esolangs> <orbitaldecay72> Corbin: thanks!
18:26:20 <Corbin> Ha, don't thank me yet. It took me a while to personally overcome old beliefs about maths and accept topos theory as a reasonable way to get things done.
18:27:03 <esolangs> <orbitaldecay72> My thinking is this. We can definitely construct a Hilbert style axiom system that allows us to prove a contradiction (we have to try hard to avoid this). If type systems are basically equivalent to these, then why can't we construct a type system in which a non-normalizing term is well typed?
18:27:12 <esolangs> <orbitaldecay72> Corbin: I'm always trying to overcome old beliefs :)
18:28:01 <esolangs> <orbitaldecay72> Again, I'm way out of my depth here. Just trying to develop some sort of intuition for the topic.
18:29:13 <Corbin> No worries. The answer I'd choose to keep going with Curry-Howard-Lambek, and do some category theory. We usually say that proofs of contradiction are rare because they can be shown to be categorically equivalent.
18:30:06 <Corbin> Categorically, an arrow into the initial object can only come from another initial object, and they're isomorphic. Logically, a proof of contradiction can only come from another contradiction, and they're equivalent.
18:30:17 <esolangs> <orbitaldecay72> Cool. I'll follow up with the category theory. Whenever I start barking about these questions I almost universally hear, "See category theory". Unfortunately I haven't done that yet, so I suppose I should!
18:30:42 -!- tromp has joined.
18:30:44 <Corbin> (Constructively, recally that a proof of contradiction ~P is literally something like "P -> false". Being able to logically entail falsity is the ur-contradiction.)
18:31:16 <esolangs> <orbitaldecay72> Corbin: But doesn't this all presuppose classical logic? i.e. what if we are using a logic in which contradiction doesn't entail everything?
18:31:26 <esolangs> <orbitaldecay72> Or am I missing the point?
18:31:54 <Corbin> Category theory's just so much neater for logic. Like, take *any* formal logic with rewrite rules. There's a category whose objects are equivalence classes of terms, and whose arrows embody the rewrite rules.
18:32:07 <esolangs> [[User:GreenThePear]] N https://esolangs.org/w/index.php?oldid=84452 * GreenThePear * (+702) Created
18:32:16 <esolangs> <orbitaldecay72> Got it. Alright, next stop category theory :)
18:32:23 <esolangs> <orbitaldecay72> Thanks so much for your help. I really appreciate it.
18:33:35 <Corbin> This all presupposes some constructive logic, but not classical logic. That's the key change in POV. And yes, it's possible to build interesting paraconsistent models, and also to require relevance for contradictions, but we don't necessarily know how to implement those in computers.
18:34:03 <Corbin> No worries. Sorry for dumping so much information onto you; hopefully it makes a little sense. Bauer's paper is really eye-opening on its own.
18:38:05 <esolangs> <orbitaldecay72> The information is great. I come here whenever I have a question that I'm having trouble answering because invariably I get a ton of information dumped on me haha
18:44:41 -!- oerjan has joined.
18:44:50 <riv> if categories are great why aren't there 2-categories?
18:47:36 <oerjan> https://golem.ph.utexas.edu/category/ (note: i'm not really a follower but i've heard about it)
18:48:15 <esolangs> [[What's the dog doin?]] https://esolangs.org/w/index.php?diff=84453&oldid=84445 * GreenThePear * (-4) /* Examples */
18:50:10 <esolangs> [[Python is Magic]] N https://esolangs.org/w/index.php?oldid=84454 * Gilbert189 * (+6954) Created page with "Python is Magic is a very restricted version of Python 3. On Python is Magic, only magic functions can be used. ==Warm-up== This is a valid Python is Magic code: __name__.__..."
18:50:24 <oerjan> https://en.wikipedia.org/wiki/Higher_category_theory might be more elucidating. (i haven't read that either.)
18:50:35 <shachaf> If cats are so great why aren't there 2-cats?
18:50:52 <oerjan> i was about to mention shachaf, i think he knows a lot more about it than i
18:51:18 <oerjan> if you can keep him from doing feline puns
18:51:41 <esolangs> [[User:Gilbert189]] https://esolangs.org/w/index.php?diff=84455&oldid=81403 * Gilbert189 * (-61)
18:51:42 <riv> https://www.reddit.com/r/confusing_perspective/comments/c95247/siamese_twins_cats/ here is a 2-cat
18:58:03 <Corbin> As a warmup, my housecat was yowling all last night. We got a little cat opera'd.
18:58:35 <Corbin> I still like "sets are 0-categories"; all of the structure of set theory is like a "decategorified" version of category theory.
19:00:57 <shachaf> Remember, booleans are just -1-categories.
19:01:46 <riv> is this true?
19:03:00 <shachaf> See https://ncatlab.org/nlab/show/negative+thinking
19:03:05 <b_jonas> one conversation about image processing and one about formal logic. I don't contribute much today, but I'm glad the channel is back to its old weird self
19:03:18 <oerjan> it slightly reminds me that certain definitions of dimension consider the empty set -1-dimensional
19:03:50 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
19:05:02 <oerjan> i'd have to look that up
19:06:31 <oerjan> https://en.wikipedia.org/wiki/Dimension#Topological_spaces starts with the lebesgue covering dimension which is an example
19:09:48 <riv> b_jonas, thanks!
19:10:02 <oerjan> seems to be true for the inductive ones too
19:52:57 <esolangs> [[Talk:Emoji-gramming]] https://esolangs.org/w/index.php?diff=84456&oldid=83822 * Qwertyu63 * (+563) /* Sign checking */
19:52:58 -!- sech1ptheythem[m has joined.
19:58:59 <b_jonas> and the weird thing is, half of the nicks I don't even recognize from earlier, and I wonder if people just took the opportunity at the network switch to choose new nicks and I'm so stupid as to not recognize them after that, but that probably isn't the case
19:59:52 <b_jonas> this channel does somehow indeed manage to pull in new weird people, even though I have no idea how they find their way here because we don't advertise ourselves very much and I find it hard to find my way into these kinds of communities
20:00:17 <b_jonas> also I have all sorts of personal problems and sometimes you help but sometimes you cause me to stay up at night when I really shoulnd't, not that I'm blaming you, just saying
20:00:48 <b_jonas> and the sad part is when that happens and I know that the other people who I'm talking to are Europeans and have a messed up sleep cycle hurting them too
20:00:55 -!- imode has joined.
20:01:20 <b_jonas> the "booleans are just -1-categories" thing sounds somehow wrong though
20:01:48 <b_jonas> or at least not true in the literal sense but perhaps there's some interesting enough analogy there that might work even if not in the literal sense
20:01:56 <riv> b_jonas, i used to be rain1
20:02:25 <b_jonas> and I knwo that moony renamed himself to, um, let me consult NAMES
20:03:19 <oerjan> b_jonas: i know at least keegan took that opportunity too
20:04:10 <b_jonas> and perhaps some old people who left #esoteric for years but stayed on freenode, they took this oppurtunity to just CHECK on which old channels move there because they wanted to know just in case, and joined, and got stuck
20:04:19 <b_jonas> because that's certainly something I'd do with other channels
20:04:51 <b_jonas> anyway, moony took a short nick and I think I'll recognize him if he returns under that
20:05:00 <nakilon> I had to change my nickname to velik
20:05:28 <b_jonas> what? "had to" but renamed the bot to the old name?
20:05:58 <nakilon> I just realised that I had to
20:05:58 <b_jonas> (well he's called "moon" now, but some people switch between nicks)
20:06:32 <b_jonas> yeah, that makes more sense even though I never felt the need, perhaps because I feel lucky for choosing b_jonas because it's a better name than I knew when I came up with it
20:06:38 <oerjan> i thought moon had always been switching nicks
20:06:45 <nakilon> I still don't know who's the pythondebugshell
20:06:49 <oerjan> but usualy not very far
20:06:56 <b_jonas> that's why I recognize him more easily
20:07:18 <b_jonas> I still don't know who Corbin is, and of course sometimes wonder about people who I do recall but don't seem to come in anymore
20:07:44 <b_jonas> although... there is a certain person who used to come in and I think used to ask about formal logic... I wonder
20:07:47 <riv> i know who Corbin is :>
20:08:19 <b_jonas> no, probably no, because I think they're from another continent
20:08:27 * oerjan looks quizzically at Corbin
20:08:29 <riv> orbitaldecay72 is the one who had that amazing stuff about bitfuck right?
20:08:43 <nakilon> "I have all sorts of personal problems" -- heh, I'm a meter away from losing a flat and being kicked out of the country, and it makes me have bad dreams every night now
20:08:57 <riv> omg that sounds horrible and stressful D:
20:10:50 <b_jonas> also, don't take this the wrong way, but hearing that from other people also makes it seem like this is back to good old #esoteric, because they're willing to share more than I do
20:11:09 <b_jonas> about their problems, that is, not that I'm too careful about letting private details on
20:14:39 <b_jonas> and I think that one terrible time when I was in a psychiatric hospital in 2018, the one I don't talk about often, part of what helped me shrug some of it off (besides my parents' care and being lucky about which doctor happened to do urgent care that night) was that I recalled that at least two different people on #esoteric told me earlier about when they were in psychiatric hospital, and I wasn't
20:14:45 <b_jonas> thinking they were in great state, but they survived being in a hospital, one even for an extended time and IRCing from there, and didn't seem to be completely broken even months after,
20:15:05 <b_jonas> plus similar stories from other weird parts of the internet
20:15:44 <b_jonas> although it also worked because at least I did learn what I really should pay attention to in order to not get back there again
20:16:35 <b_jonas> I just rarely feel stupid enough to discuss it in logged and googleable parts of the internet, especially as I know my nick isn't all that secret
20:18:01 <b_jonas> and it would have been wiser to use a disposable alternate nick, if not now, at least that one time when I posted about it to a forum
20:19:35 <nakilon> woah, there are at least three people here who were in psychiatric hospitals?
20:20:27 <riv> I do miss some of the people who used to come here
20:22:14 <nakilon> I would probably not mind to get stuck in anywhere as long as there are some family members or friends to take care of your home, bills, hypothetical cat, etc.
20:22:31 <riv> lol, hypothetical cat
20:27:09 -!- tromp has joined.
20:32:14 <b_jonas> at least if you count people who used to be here at some point but might not visit now
20:34:04 <b_jonas> I wasn't *stuck*. it was a short time, I knew I'd get out soon, that's what the doctor said to me and she was right, and once she even allowed me to temporarily leave for a few hours in what she said was against the hospital's rules (not that I have illusions about those rules consistently being kept) because my family promised to bring me back
20:34:36 <b_jonas> it's the at least one other user, the one who IRCed from the hospital, regularly, who was stuck
20:35:30 <b_jonas> I don't pretend that I'm not stuck with a psychiatric condition that I'd have to be careful with for my whole life even if I managed to get my life mostly normal, but I was not stuck in the hospital
20:59:01 <b_jonas> also hi future boss, who will probably find this months or years from now when searching for my name, I know you're listening and want to find out what I'm hiding by looking on the internet and asking previous employers' opinions, and you're going to pay me less money if you don't just reject me completely, but I think I wouldn't want to work in a company that has managers less diligent than that, I
20:59:07 <b_jonas> couldn't trust that they could keep themselves in the business
21:04:37 -!- sech1ptheythem[m has quit (Remote host closed the connection).
21:04:39 -!- jryans has quit (Read error: Connection reset by peer).
21:05:54 -!- jryans has joined.
21:06:31 -!- dbohdan has quit (Read error: Connection reset by peer).
21:06:36 -!- arseniiv has quit (Ping timeout: 245 seconds).
21:06:41 -!- riv has quit (Read error: Connection reset by peer).
21:06:41 -!- arseniiv_ has joined.
21:06:51 -!- dbohdan has joined.
21:07:22 -!- citrons has quit (Ping timeout: 252 seconds).
21:08:11 -!- citrons has joined.
21:08:44 -!- Trieste_ has joined.
21:09:05 -!- moon5 has joined.
21:09:48 -!- moon has quit (Killed (copper.libera.chat (Nickname regained by services))).
21:09:48 -!- moon5 has changed nick to moon.
21:12:24 -!- sech1ptheythem[m has joined.
21:12:25 -!- int-e_ has joined.
21:12:49 -!- Trieste has quit (Quit: Be well!).
21:14:46 -!- zegalch has quit (Quit: Ping timeout (120 seconds)).
21:14:47 -!- int-e has quit (Ping timeout: 264 seconds).
21:14:47 -!- HackEso has quit (Ping timeout: 264 seconds).
21:14:58 -!- Sgeo_ has joined.
21:15:11 -!- riv has joined.
21:15:53 -!- zegalch has joined.
21:17:44 -!- moon2 has joined.
21:18:20 -!- moon has quit (Killed (iridium.libera.chat (Nickname regained by services))).
21:18:20 -!- moon2 has changed nick to moon.
21:19:09 -!- Trieste has joined.
21:21:28 -!- citrons_ has joined.
21:22:04 -!- ski has quit (Ping timeout: 265 seconds).
21:22:04 -!- integral has quit (Ping timeout: 265 seconds).
21:22:23 -!- ski has joined.
21:22:47 -!- imode has changed nick to FuckAndrewLee.
21:23:02 -!- Lord_of_Life_ has joined.
21:23:18 -!- perlbot_ has joined.
21:23:34 -!- integral has joined.
21:24:51 -!- perlbot has quit (Ping timeout: 265 seconds).
21:24:51 -!- yuu has quit (Ping timeout: 265 seconds).
21:24:53 -!- Trieste_ has quit (*.net *.split).
21:24:53 -!- citrons has quit (*.net *.split).
21:24:54 -!- Sgeo has quit (*.net *.split).
21:24:54 -!- Lord_of_Life has quit (*.net *.split).
21:24:54 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
21:25:03 -!- perlbot_ has changed nick to perlbot.
21:25:32 -!- lifthrasiir has quit (Read error: Connection reset by peer).
21:25:49 -!- V has quit (Ping timeout: 265 seconds).
21:26:28 -!- V has joined.
21:26:40 -!- lifthrasiir has joined.
21:27:01 -!- yuu has joined.
21:27:38 -!- HackEso has joined.
21:27:52 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
21:28:29 <shachaf> Happy pigeon appreciation day!
21:32:07 -!- FuckAndrewLee has changed nick to rusted-root.
21:35:39 <aarchi> Does anyone by chance have a copy of the HaPyLi compiler? It's a Haskell/Python/Lisp-like language that compiles to Whitespace.
21:36:41 <aarchi> The website went offline around 2012 and it wasn't completely archived on the Internet Archive.
21:36:43 -!- tromp has joined.
21:44:21 -!- rusted-root has changed nick to imode.
21:44:24 -!- freon has quit (Ping timeout: 250 seconds).
21:56:52 * pikhq counts herself very glad nobody else wants pikhq
21:57:36 <pikhq> riv: yeah, i miss some people who used to be here too. still in touch with some though i don't talk with them much; also still frequently in touch with others
21:57:51 <riv> oh that's nice
21:58:23 <pikhq> and re: psych hospital. glad i've never been in one but fuck i've been close
22:00:03 <pikhq> turns out being into absolutely weird programming languages has a high overlap with just being weird as a person in one of a few different ways
22:01:53 <esolangs> [[User:Zzo38/Programming languages with unusual features]] https://esolangs.org/w/index.php?diff=84457&oldid=84358 * Zzo38 * (+94) The {edit} macro in Free Hero Mesh
22:11:25 <pikhq> i mean i am very much a weird person so :p
22:22:40 <b_jonas> pikhq: yes, but how do so many of those kinds of people actually find their way here, that's what I don't understand
22:24:13 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
22:24:46 <b_jonas> I don't understand that even after I just personally recommended this channel to someone and they came here
22:25:09 <b_jonas> because how did I find them in first place
22:25:17 <pikhq> if you're that sort of weird you're gonna actively seek it out
22:26:59 <zzo38> I don't have a copy of the HaPyLi
22:32:01 <esolangs> [[Special:Log/newusers]] create * Hjoker4 * New user account
22:36:00 -!- imode has changed nick to ch0de.
22:49:13 <zzo38> Do you like the picture editor of Free Hero Mesh?
22:56:32 -!- salpynx has joined.
23:06:39 -!- user3456 has quit (Quit: ZNC - https://znc.in).
23:07:42 <zzo38> Will they add the Quasijarus compression format into newer versions of GNU/Linux and/or non-Quasijarus BSD?
23:08:38 -!- user3456 has joined.
23:14:51 <esolangs> [[Among Us]] https://esolangs.org/w/index.php?diff=84458&oldid=84356 * Zero player rodent * (+211)
23:18:03 <sknebel> if you ever dig into esolangs even a bit and want to talk to people into them this channel is hard to not find. the esolangs wiki is like the resource referenced everywhere after all
23:26:28 <pikhq> hence how i found it when i was, like, 15
23:29:15 -!- tech_exorcist has quit (Quit: tech_exorcist).
23:40:42 <esolangs> [[Among Us]] https://esolangs.org/w/index.php?diff=84459&oldid=84458 * Zero player rodent * (+99)
23:47:01 <esolangs> [[VBF]] M https://esolangs.org/w/index.php?diff=84460&oldid=84440 * PythonshellDebugwindow * (+53) /* Implementations */ Cats
23:47:51 <esolangs> [[Among Us]] https://esolangs.org/w/index.php?diff=84461&oldid=84459 * Zero player rodent * (+149)
23:48:24 <esolangs> [[GotoFuck]] M https://esolangs.org/w/index.php?diff=84462&oldid=83713 * PythonshellDebugwindow * (+78) /* Implementations */ Cats, see also
23:48:41 <esolangs> [[Jumplang]] M https://esolangs.org/w/index.php?diff=84463&oldid=74090 * PythonshellDebugwindow * (+15) /* See also */ See also.
23:53:25 <esolangs> <orbitaldecay17> riv: yep! I was playing around with bitfuck a few years ago.
23:53:57 <esolangs> <orbitaldecay17> specifically messing around with the reversible variant, which permits some interesting minimizations