06:15:46 <esolangs> [[Marble]] M https://esolangs.org/w/index.php?diff=119799&oldid=119798 * PythonshellDebugwindow * (+84) Categories
07:11:47 -!- tromp has joined.
07:15:50 -!- ais523 has quit (Quit: quit).
08:45:18 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
09:03:50 -!- cpressey has joined.
09:26:51 -!- Koen has joined.
09:44:33 <esolangs> [[Talk:Cutw]] https://esolangs.org/w/index.php?diff=119800&oldid=119761 * None1 * (+22)
09:45:33 <esolangs> [[Special:Log/newusers]] create * Joulier429 * New user account
09:47:18 <esolangs> [[Template talk:Py]] https://esolangs.org/w/index.php?diff=119801&oldid=119795 * None1 * (+133) /* ...this is already a thing though? */
09:50:43 <cpressey> So I've been thinking. The adequacy of the LCF approach really depends on your "threat model". If you just want to protect against mistakes, it's enough (possibly even more than you need), but if you want to defend against someone *falsifying* a proof, though, it needs to be supplemented (by checking a produced certificate).
09:52:10 <cpressey> Because of ROTT, right? Even if your proof language makes 100% guarantees about integrity of your data structures, who knows what the compiler that compiled the implementation of your proof language might've snuck in there.
09:53:11 <cpressey> Anyway, it's the beauty of the idea "Abstract Data Type = Algebra = Proof System" that appeals to me, not really these practical matters.
09:55:34 -!- tromp has joined.
10:06:31 -!- Lord_of_Life has quit (Ping timeout: 255 seconds).
10:07:13 -!- Lord_of_Life has joined.
10:13:08 <cpressey> "possibly even more than you need" -> Programmers get by with a lot less on a daily basis. "Voluntary encapsulation" in popular languages. Otoh, a lot of software in production has data integrity holes in it. Sometimes massive ones. So that's probably not a good basis for comparison.
11:02:50 <esolangs> [[4RL]] https://esolangs.org/w/index.php?diff=119802&oldid=96987 * Kaveh Yousefi * (+183) Added a hyperlink to my implementation of the 4RL programming language on GitHub and added the category tag Implemented.
11:07:44 <esolangs> [[4RL]] https://esolangs.org/w/index.php?diff=119803&oldid=119802 * Kaveh Yousefi * (+517) Supplemented three further example programs, namely (1) a repeating cat program, (2) a truth-machine, and (3) a program termination demonstrator.
11:08:06 <b_jonas> sure, but automatically producing a certificate and checking it elsewhere is the easy part. the hard part is making the language convenient enough to express long proofs easily, and also making sure that humans can check all your aximos and the statement of theorems easily (because a proof isn't worth much if you aren't sure what it proves)
11:18:55 -!- arseniiv has joined.
11:23:26 <cpressey> A language that makes something convenient?? Perish the thought, in this channel!
11:39:45 -!- Sgeo has quit (Read error: Connection reset by peer).
12:16:05 -!- __monty__ has joined.
13:05:13 -!- Koen has quit (Remote host closed the connection).
13:32:45 -!- Koen has joined.
13:37:35 -!- Koen has quit (Remote host closed the connection).
13:38:38 -!- Koen has joined.
13:40:21 -!- Koen has quit (Remote host closed the connection).
13:44:27 <arseniiv> a language with the sole (or almost sole) numeric operation which is arithmetic-geometric mean
14:27:37 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
14:36:37 <b_jonas> arseniiv: we have languages with a restricted set of arithmetic operations: Nellephant which uses attract and repel, which I find very annoying and unnecessary because it doesn't seem to really help what that language is trying to do over using more sane arithmetic operations; and more interestingly Analogia
14:37:23 <b_jonas> also possibly Conedy, depending on how you interpret "numeric operations"
14:42:02 <arseniiv> b_jonas: oh I read only today that “analogia” is Ancient Greek for hm I forgot what in arithmetic but something basic
14:53:52 <b_jonas> man, we should've just left the babylonians and arabs develop mathematics and science and astronomy. the ancient greeks like Euclid and especially Aristoteles just made everything worse. their only upside was Archimedes.
14:55:11 <b_jonas> plus the Mayans could help if we can contact them earlier I guess
15:07:19 -!- Koen has joined.
15:24:38 -!- tromp has joined.
15:35:16 -!- cpressey has quit (Ping timeout: 250 seconds).
15:46:27 -!- cpressey has joined.
15:47:34 <esolangs> [[Funky]] https://esolangs.org/w/index.php?diff=119804&oldid=119597 * DaMutasimos * (+17)
15:49:19 <esolangs> [[Funky]] https://esolangs.org/w/index.php?diff=119805&oldid=119804 * DaMutasimos * (+0) /* Creating custom functions */
15:50:55 <esolangs> [[Funky]] https://esolangs.org/w/index.php?diff=119806&oldid=119805 * DaMutasimos * (+11) /* Creating custom functions */
15:52:44 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
15:55:37 <esolangs> [[Talk:A Language Programmed While Listening to Godspeed You! Black Emperor]] N https://esolangs.org/w/index.php?oldid=119807 * DaMutasimos * (+34) Created page with "otherwise known as ALPWLTGYBE?!?!?"
15:57:30 -!- tromp has joined.
16:02:20 -!- ais523 has joined.
17:31:04 <esolangs> [[Special:Log/newusers]] create * Fdai * New user account
17:43:32 -!- cpressey has quit (Ping timeout: 250 seconds).
18:07:51 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
18:25:16 -!- tromp has joined.
18:34:55 -!- Hooloovoo has quit (Ping timeout: 245 seconds).
18:37:35 -!- Hooloovoo has joined.
19:01:48 -!- Melvar has quit (Quit: WeeChat 4.1.0).
19:13:11 -!- ais523 has quit (Quit: playing in a bridge tournament).
19:23:32 -!- zzo38_ has joined.
19:26:24 -!- zzo38 has quit (Ping timeout: 252 seconds).
19:36:59 -!- Melvar has joined.
19:54:29 -!- Koen has quit (Quit: Leaving...).
19:56:17 -!- zzo38_ has changed nick to zzo38.
20:18:17 -!- cpressey has joined.
20:50:06 <esolangs> [[Wiwa]] N https://esolangs.org/w/index.php?oldid=119808 * 0ptr * (+7334) Created page with "'''Wiwa''' is a stack-based, array-oriented esolang inspired by [Uiua https://uiua.org] and [BQN https://mlochbaum.github.io/BQN]. '''Wiwa''' operates on a stack of arrays. Each array can only contain other arrays, meaning there are no values in Wiwa. You can find the inter
20:50:18 <esolangs> [[Wiwa]] M https://esolangs.org/w/index.php?diff=119809&oldid=119808 * 0ptr * (+0) fix the link
20:50:41 <esolangs> [[Wiwa]] M https://esolangs.org/w/index.php?diff=119810&oldid=119809 * 0ptr * (+0) fix links
20:55:27 <esolangs> [[Wiwa]] M https://esolangs.org/w/index.php?diff=119811&oldid=119810 * 0ptr * (-8)
21:05:56 <arseniiv> <b_jonas> their only upside was Archimedes. => he was
21:11:51 -!- arseniiv has quit (Quit: gone too far).
21:45:30 <esolangs> [[Turing Tumble]] M https://esolangs.org/w/index.php?diff=119812&oldid=52228 * PythonshellDebugwindow * (+9) Stub
21:51:03 -!- Sgeo has joined.
22:05:34 -!- zzo38 has quit (Ping timeout: 276 seconds).
22:16:00 <esolangs> [[Alphuck]] https://esolangs.org/w/index.php?diff=119813&oldid=119760 * Kaveh Yousefi * (+121) Added a repeating cat program and subsumed the twissel of extant examples into a common section.
22:18:29 -!- ais523 has joined.
22:20:19 <esolangs> [[Alphuck]] https://esolangs.org/w/index.php?diff=119814&oldid=119813 * Kaveh Yousefi * (+3803) Added an interpreter implementation in Common Lisp.
22:21:00 -!- cpressey has quit (Quit: Client closed).
22:22:27 -!- __monty__ has quit (Quit: leaving).
22:23:37 <esolangs> [[Alphuck]] https://esolangs.org/w/index.php?diff=119815&oldid=119814 * Kaveh Yousefi * (+233) Improved the command table's formatting and supplemented the page category tag Implemented.
22:35:47 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
22:47:42 -!- tromp has joined.
23:00:57 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
23:07:55 -!- zzo38 has joined.
23:16:51 -!- zzo38 has quit (Ping timeout: 252 seconds).
23:18:12 -!- zzo38 has joined.
23:18:27 -!- zzo38 has changed nick to zzo38_.
23:18:35 -!- zzo38_ has changed nick to zzo38.
23:27:08 -!- zzo38 has quit (Killed (NickServ (GHOST command used by zzo38_))).
23:27:21 -!- zzo38 has joined.