< 1582678230 888165 :zzo38!~zzo38@host-24-207-50-7.public.eastlink.ca PRIVMSG #esoteric :I played GURPS game today. Now in addition to Ziveruskex and Strixan is also Iuckqlwviv Kjugobe, who has a astrolabe, Fanucci deck, pet leech, robe, and quarterstaff (which he traded for a magic quarterstaff, but intend to trade back later). Kjugobe is also psychic. < 1582678232 834497 :zzo38!~zzo38@host-24-207-50-7.public.eastlink.ca PRIVMSG #esoteric :But the princess got lost and they blamed us for it. But I found some sort of magic tree, the parallax doesn't looks like properly, but then we went there and found ourself in some kind of desert with a lot of sand (including wind). < 1582678383 86826 :imode!~linear@unaffiliated/imode JOIN :#esoteric < 1582679229 926411 :zzo38!~zzo38@host-24-207-50-7.public.eastlink.ca PRIVMSG #esoteric :Do you like this? < 1582679542 628179 :FreeFull!~freefull@defocus/sausage-lover QUIT : < 1582680345 168116 :b_jonas!~x@catv-176-63-14-29.catv.broadband.hu PRIVMSG #esoteric :zzo38: ooh, that part about the tree and desert sounds like Jimmy Knopf < 1582680412 601557 :zzo38!~zzo38@host-24-207-50-7.public.eastlink.ca PRIVMSG #esoteric :Who is Jimmy Knopf? < 1582684301 947306 :oerjan!oerjan@sprocket.nvg.ntnu.no JOIN :#esoteric < 1582684758 856983 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :the birth of ennesquid < 1582684766 685241 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric : < 1582685393 997456 :zzo38!~zzo38@host-24-207-50-7.public.eastlink.ca PRIVMSG #esoteric :What is that? < 1582685450 289457 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :latest schlock mercenary < 1582686196 581088 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :`olist 1193 < 1582686198 365797 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :olist 1193: shachaf oerjan Sgeo FireFly boily nortti b_jonas < 1582686972 106641 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :@metar ENVA < 1582686972 597021 :lambdabot!~lambdabot@haskell/bot/lambdabot PRIVMSG #esoteric :ENVA 260250Z 12006KT CAVOK M11/M13 Q0998 RMK WIND 670FT 10009KT < 1582687402 88556 :imode!~linear@unaffiliated/imode QUIT :Ping timeout: 255 seconds < 1582690806 707642 :zzo38!~zzo38@host-24-207-50-7.public.eastlink.ca PRIVMSG #esoteric :But the Sun is almost directly overhead, therefore we are probably close to the equator (it is the equinox), and this is a small astrolabe without interchangeable plates, so some of the functions will not work at this latitude unless it is a magic astrolabe that can automatically recalibrate itself. < 1582691484 976697 :xkapastel!uid17782@gateway/web/irccloud.com/x-kkzhkmuwvaoqtofm JOIN :#esoteric < 1582693414 850283 :imode!~linear@unaffiliated/imode JOIN :#esoteric < 1582695883 803687 :xelxebar!~xelxebar@gateway/tor-sasl/xelxebar QUIT :Remote host closed the connection < 1582696003 694707 :xelxebar!~xelxebar@gateway/tor-sasl/xelxebar JOIN :#esoteric < 1582697151 862491 :arseniiv!~arseniiv@95.105.14.199.dynamic.ufanet.ru JOIN :#esoteric < 1582697332 809986 :xelxebar!~xelxebar@gateway/tor-sasl/xelxebar QUIT :Remote host closed the connection < 1582697356 127586 :Sgeo_!~Sgeo@ool-18b982ad.dyn.optonline.net QUIT :Read error: Connection reset by peer < 1582697382 921358 :Sgeo_!~Sgeo@ool-18b982ad.dyn.optonline.net JOIN :#esoteric < 1582698809 631381 :arseniiv!~arseniiv@95.105.14.199.dynamic.ufanet.ru PRIVMSG #esoteric :`? password < 1582698811 709908 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :The password of the month is leapfrogging rats. < 1582698892 762451 :arseniiv!~arseniiv@95.105.14.199.dynamic.ufanet.ru PRIVMSG #esoteric :leap earring < 1582698946 290542 :arseniiv!~arseniiv@95.105.14.199.dynamic.ufanet.ru PRIVMSG #esoteric :it would be silly and wonderful if we didn’t know if the current year is leap until it almost ends < 1582698972 531397 :arseniiv!~arseniiv@95.105.14.199.dynamic.ufanet.ru PRIVMSG #esoteric :with the mechanism like something with leap seconds, I presume? < 1582700690 848942 :imode!~linear@unaffiliated/imode QUIT :Ping timeout: 240 seconds < 1582701851 436303 :ArthurStrong!~ArthurStr@slow.wreckage.volia.net JOIN :#esoteric < 1582701968 110969 :xelxebar!~xelxebar@gateway/tor-sasl/xelxebar JOIN :#esoteric < 1582702123 932184 :xelxebar!~xelxebar@gateway/tor-sasl/xelxebar QUIT :Remote host closed the connection < 1582702150 699412 :xelxebar!~xelxebar@gateway/tor-sasl/xelxebar JOIN :#esoteric < 1582702580 140549 :Lord_of_Life_!~Lord@unaffiliated/lord-of-life/x-0885362 JOIN :#esoteric < 1582702619 362646 :Lord_of_Life!~Lord@unaffiliated/lord-of-life/x-0885362 QUIT :Ping timeout: 272 seconds < 1582702660 593090 :Lord_of_Life_!~Lord@unaffiliated/lord-of-life/x-0885362 NICK :Lord_of_Life > 1582703327 866605 PRIVMSG #esoteric :14[[07User talk:Oklomsy14]]4 10 02https://esolangs.org/w/index.php?diff=70054&oldid=68946 5* 03Oklomsy 5* (+125) 10/* New language idea maybe. */ new section > 1582703366 287443 PRIVMSG #esoteric :14[[07User talk:Oklomsy14]]4 10 02https://esolangs.org/w/index.php?diff=70055&oldid=70054 5* 03Oklomsy 5* (+66) 10/* New language idea maybe. */ < 1582705639 808402 :int-e!~noone@int-e.eu PRIVMSG #esoteric :fungot: what's my motivation? < 1582705640 4386 :fungot!~fungot@unaffiliated/fizzie/bot/fungot PRIVMSG #esoteric :int-e: you mean demoscene.tv requires proprietary software? :) fnord/ compilers/ linguine/ linguine.py': errno 13 permission denied: ' lament' < 1582705695 825901 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :the proprietary fnord suite, the bane of demosceners everywhere < 1582705901 498060 :ArthurStrong!~ArthurStr@slow.wreckage.volia.net QUIT :Quit: leaving < 1582705960 366533 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Freefall isn't helping my motivation either. < 1582705976 161726 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(Monday's that is) < 1582706046 719043 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :'s ok sam will fix it all he just needs to get a green cloak for proper style < 1582706093 538633 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :s/cloak/outfit/ < 1582706138 820236 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :today's girl genius went about as i'd expected < 1582706154 693866 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :(vaguely) < 1582706174 696178 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Nice reminder of the hat though. < 1582706241 179316 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :there were way too many scenes in comic where gil _should_ have noticed. < 1582706418 80920 :int-e!~noone@int-e.eu PRIVMSG #esoteric :But Gil never notices anything, except when it matters. < 1582706456 359966 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :i'm pretty sure it's been pointed out that he notices more than he lots on < 1582706471 715291 :oerjan!oerjan@sprocket.nvg.ntnu.no PRIVMSG #esoteric :*lets < 1582706527 91362 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Not that I noticed ;) < 1582706591 5547 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(No, it has definitely been pointed out that he notices a lot more than he lets on. There have also been some interesting fights that he won way too casually.) < 1582707564 577369 :b_jonas!~x@catv-176-63-14-29.catv.broadband.hu QUIT :Quit: leaving < 1582708621 90873 :cpressey!~cpressey@5.133.242.4 JOIN :#esoteric < 1582708851 734603 :xkapastel!uid17782@gateway/web/irccloud.com/x-kkzhkmuwvaoqtofm QUIT :Quit: Connection closed for inactivity < 1582708852 814714 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :int-e: Now that your paper is safely submitted to AFP, I could give you my feedback. < 1582708928 636180 :int-e!~noone@int-e.eu PRIVMSG #esoteric :cpressey: I might feel obliged to update it... < 1582708981 706655 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(there is a process for that; what happens is that the update ends up in the development version and in future AFP releases. AFP-2020 will appear at some point.) < 1582708997 131197 :int-e!~noone@int-e.eu PRIVMSG #esoteric :The old versions are archived, so it's still transparent. < 1582709008 767393 :int-e!~noone@int-e.eu PRIVMSG #esoteric :cpressey: But sure, go ahead if you like. < 1582709477 303446 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :"omg in Isabelle/HOL the expression for G_16 cannot be typed?! lol l/\m3" < 1582709485 711835 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :See, I didn't think you'd find it useful. < 1582709618 318703 :int-e!~noone@int-e.eu PRIVMSG #esoteric :cpressey: Yeah that isn't useful. I even mention it in the paper :P I didn't mention Coq or Agda, because I really didn't want go looking for the proper references. < 1582709670 955484 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(Or figure out whether there should be more ITPs or programming languages on that list.) < 1582710322 580504 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :It was more of a reaction than feedback, I suppose. But on the subject of ITPs. I've been toying with the idea of learning one, but I don't have many strong feelings towards any of them. < 1582710346 760829 :longname!~airbouy@75-26-238-119.lightspeed.glvwil.sbcglobal.net QUIT :Read error: Connection reset by peer < 1582710360 915871 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :I am tickled by the fact that Isabelle has "moreover" and "ultimately" keywords. < 1582710496 15605 :int-e!~noone@int-e.eu PRIVMSG #esoteric :cpressey: It also has 'also' and 'finally'. < 1582710509 44116 :longname!~airbouy@75-26-238-119.lightspeed.glvwil.sbcglobal.net JOIN :#esoteric < 1582710510 153255 :int-e!~noone@int-e.eu PRIVMSG #esoteric :cpressey: Which are for chaing (in)equalities. < 1582710527 877537 :int-e!~noone@int-e.eu PRIVMSG #esoteric :*chaining* (is that an auto-portmonteau?) < 1582710774 977037 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :int-e: Have you seen https://github.com/avigad/arwm ? I found the slides interesting, haven't read the notes yet. < 1582710927 886480 :int-e!~noone@int-e.eu PRIVMSG #esoteric :No I have not. < 1582710956 900977 :int-e!~noone@int-e.eu PRIVMSG #esoteric :August 2019, hmm. < 1582711258 947250 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Well, not sure how I could've found out either; for example, I don't see anything on the isabelle users mailing list... < 1582711269 680702 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(though perhaps I missed it) < 1582711836 971115 :xkapastel!uid17782@gateway/web/irccloud.com/x-oolslzdmrjfvdmwr JOIN :#esoteric < 1582712111 547994 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :Gah, looking over all the choices again, I still can't decide, and I forget why I wanted to do this again? < 1582712529 701152 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I've been meaning to look at Lean for a while now. Learning any ITP is a major investment of time, and if you formalize anything non-trivial, it's bound to be an exercise in frustration (you may expect to spend 90% of your time on proving obvious things, or thinking of ways to avoid that kind of dive into trivialities). < 1582712595 623618 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(One of the running gags is that formalizing a paper proof is easy until you run into the word "obviously".) < 1582712835 268251 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I think both Coq and Isabelle/HOL are very formiddable contenders. HOL4 and HOL Light have large bodies of formalizations as well. Lean is a promising new project. And there's a lot of things I know exist but know little about Mizar strives to be accessible (and definitely inspired Isabelle's Isar proof language). ACL2 is huge but again I know fairly little about it. PVS is probably on its way... < 1582712841 276692 :int-e!~noone@int-e.eu PRIVMSG #esoteric :...out. Agda is more of a programming language. I'm sure I'm missing a ton of other stuff. < 1582713077 219922 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Coq will work better for shallow embeddings of PL stuff (and I don't see Isabelle/HOL growing strong in the PL area for this reason...). Isabelle/HOL commits to classical reasoning very early on, which has advantages for reusability: Only one kind of sets, only one kind of natural numbers. There's also a big formalization of real numbers and analysis included... nbot sure how Coq does there. < 1582713275 74190 :int-e!~noone@int-e.eu PRIVMSG #esoteric :cpressey: Now you sound more like a PL person to me, so I'd reluctantly recommend Coq. I like Isabelle/HOL better (largely because of the nicer proof language). < 1582713289 420831 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(And of course because I've used it way more than Coq.) < 1582713634 878254 :int-e!~noone@int-e.eu PRIVMSG #esoteric :But I also think the builtin proof tactics in Isabelle/HOL are just better. The number of proofs that are solved by 'auto' (which combines rewriting and classical reasoning for quantifiers, sets, and the like) is fairly amazing... I have not found a Coq equivalent yet (the two parts, rewriting and refining goals by introduction and elimination rules, only exist separately, as far as I've figured... < 1582713640 835081 :int-e!~noone@int-e.eu PRIVMSG #esoteric :...it out) < 1582713722 519716 :int-e!~noone@int-e.eu PRIVMSG #esoteric :But experience counts for so much in this area... that Goodstein thing could easily become twice as long without a couple of tricks that I've learned over the years. < 1582713776 585550 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Basically I've built an intuition for what auto can and cannot do. I can't fully explain it. And I don't have anything approaching that for Coq's proof tactics. < 1582713941 359824 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(And if you look inside that theory you'll see that many 'auto' uses come with extra hints (additional simplification and introduction rules, mostly.... sometimes flipping a simplification rule because the default direction of rewriting happens to hurt the proof in this particular case); there's a lot going on under the surface (a result of exploring the proof goal interactively and then... < 1582713947 354483 :int-e!~noone@int-e.eu PRIVMSG #esoteric :...extracting those hints for auto from that). < 1582714030 74810 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Hmm, long monologue. Oh well, this is about 6 years of my life. < 1582714268 306294 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :int-e: Thank you. I was in fact leaning towards Coq (yesterday, before I started wondering why I wanted to do this again). < 1582714655 938559 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :My interests in this area are difficult to explain, even to myself. It's not like I have a great deal of mathematics laying around that I want to formalize. To some degree, I'm interested in proof languages per se, as computer languages, just as programming languages are. < 1582714678 250781 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :I tried to learn Agda once. It didn't go well. < 1582714691 729832 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I've actually used Coq a little bit: https://github.com/int-e/coq-playground/ (there's both a Coq and an Isabelle/HOL version of Dilworth's theorem in there. The Isabelle version is shorter, but it's not a fair comparison; I wrote the Isabelle version *after* the Coq version, so some of the compression is from understanding the proof better; another part is of course that I have much more... < 1582714697 643017 :int-e!~noone@int-e.eu PRIVMSG #esoteric :...experience with Isabelle/HOL. I still think that Coq is a tad worse at arithmetic (which does come up a few times). < 1582714816 14752 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :I have the following very general problem: dependent types rub me the wrong way. I would have to learn to put that aside before I would be able to get very far with anything where type-value dependence is prominent. < 1582714842 339709 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(Both developemnts have a huge monolithic proof at their core... Dilworth's theorem just keeps stacking more and more information extracted from the setup until finally it all combines into a successful conclusion. This means that factoring the proof would result in lemmas with tons of assumptions. The formalization is embarrassingly large compared to the paper proof; compare... < 1582714848 337638 :int-e!~noone@int-e.eu PRIVMSG #esoteric :...https://en.wikipedia.org/wiki/Dilworth%27s_theorem#Inductive_proof . < 1582714880 188459 :int-e!~noone@int-e.eu PRIVMSG #esoteric :cpressey: Oh I'm not a huge fan of dependent types either *especially* for programming. < 1582714968 246584 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Maybe it's a matter of having convenient coercions for the common case that you don't want to prove anything about your program and just get on with it. < 1582715002 77637 :int-e!~noone@int-e.eu PRIVMSG #esoteric :("trust me, I know that n+m = m+n for natural numbers") < 1582715018 681169 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :I like dependent types but mostly because I find them fun < 1582715036 350106 :int-e!~noone@int-e.eu PRIVMSG #esoteric :I'm less dismissive of their use in ITPs though. < 1582715056 18212 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Since there the purpose is to prove everything rigorously. < 1582715126 364302 :int-e!~noone@int-e.eu PRIVMSG #esoteric :So it's more about expressiveness of the term language, and more expressiveness is usually better. (There's a cost to this... automatic proof methods have to deal with those types, so that gets harder.) < 1582715126 640003 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :int-e: I know Agda has "trustMe : ∀ {a} {A : Set a} {x y : A} → x ≡ y", is this the kind of coercion you're after? < 1582715152 816058 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Taneb: That's the kind of thing I'm after, yes. Except that's too verbose. < 1582715290 705699 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Btw, I have not actually tried to use Agda; this is speculation, somewhat educated by working with constraints (and, to a far lesser extent, type literals) in Haskell. < 1582715299 21563 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :Have you tried Lean? (disclaimer: I have not). I believe there you can do as much or as little proving as you like, but I may be mistaken < 1582715330 464043 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Taneb: I've been meaning to look at Lean for a while now. < 1582715352 657860 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :Ah, I didn't see that < 1582715353 536778 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(No, I can't really blame you for not reading all that.) < 1582715386 875168 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(Especially since I am terrible at catching up on context myself.) < 1582715736 866735 :oerjan!oerjan@sprocket.nvg.ntnu.no QUIT :Quit: Nite < 1582715737 92539 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :There are a few ITPs based on set theory (Metamath, mainly) but they're a definite minority. The general feeling seems to be, if you want to formalize mathematics, you want to avoid set theory, you want to use type theory instead, so that some ill-defined things can't even be stated. < 1582715814 798283 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :And then, beyond that, most of those ITPs use a type theory with dependent types, because more expressive. But is there any space for an ITP based on a non-depedent type theory? < 1582715841 462256 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :Like (just blue-skying here) System F, or System F_omega? < 1582715882 484036 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :(Or do you just get a programming language if you try that?) < 1582715940 193938 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :I keep meaning to mess around more with metamath < 1582716012 795341 :int-e!~noone@int-e.eu PRIVMSG #esoteric :cpressey: I think I would like a System F ITP. But I'm not sure where it should come from... I mean these systems are typically developed in Academia and what can you publish about this? Any reviewer will say "but we already have Coq which does more"... < 1582716056 838106 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(But as usual this may be my lack of imagination.) < 1582716237 409256 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :It could come from the burgeoning field of esoteric proof languages... :) < 1582716249 641827 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :Or it could if I had more spare time < 1582716301 475814 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Well, making a /usable/ ITP is a huge effort. < 1582716312 834964 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :No argument there < 1582716881 402380 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :On a different note, this year I learned what a "fexpr" and what the "vau-calculus" is, and realized this is basically what Robin is. (I borrowed the idea from PicoLisp, which doesn't use that terminology at all.) < 1582716928 178336 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :And realized that conventional exception handling is (roughly speaking) dynamically scoped and therefore technically violates referential transparency. < 1582719591 263036 :arseniiv!~arseniiv@95.105.14.199.dynamic.ufanet.ru PRIVMSG #esoteric : I am tickled by the fact that Isabelle has "moreover" and "ultimately" keywords. cpressey: It also has 'also' and 'finally'. => wow! Though, `finally` isn’t that new after languages with C-like syntax and exceptions < 1582719728 464227 :int-e!~noone@int-e.eu PRIVMSG #esoteric :arseniiv: Well, it doesn't have "throw". < 1582719862 125955 :arseniiv!~arseniiv@95.105.14.199.dynamic.ufanet.ru PRIVMSG #esoteric :int-e: I propose adding “throw” somewhere as a comment marker, like in “throw that human language text away” :D < 1582719963 642731 :iczero!iczero@hellomouse/dev/iczero QUIT :Excess Flood < 1582719967 943013 :Bowserinator!Bowserinat@hellomouse/dev/Bowserinator QUIT :Ping timeout: 252 seconds < 1582719983 310700 :iczero!iczero@hellomouse/dev/iczero JOIN :#esoteric < 1582719987 188522 :arseniiv!~arseniiv@95.105.14.199.dynamic.ufanet.ru PRIVMSG #esoteric :re esoteric proof languages: are there any? (and I’m almost hooked but I can’t say I could try making one myself, I have too little experience with things for simplifying proving in the real proof assistant thingies, so the image would be incomplete) < 1582719999 16758 :Bowserinator!Bowserinat@hellomouse/dev/Bowserinator JOIN :#esoteric < 1582720391 200954 :int-e!~noone@int-e.eu PRIVMSG #esoteric :arseniiv: can you name a non-esoteric one... < 1582720448 100800 :arseniiv!~arseniiv@95.105.14.199.dynamic.ufanet.ru PRIVMSG #esoteric :int-e: erm, don’t Isabelle, Coq, Agda mentioned above count? < 1582720530 429403 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :I have https://github.com/catseye/Maxixe but it's hardly esoteric. < 1582720545 461801 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :Metamath's syntax certainly *looks* esoteric. < 1582720658 615467 :int-e!~noone@int-e.eu PRIVMSG #esoteric :arseniiv: I may have been somewhat facetious there. :P < 1582720768 965378 :int-e!~noone@int-e.eu PRIVMSG #esoteric :arseniiv: My more serious thought process went in the direction of minimal logic, pure Hilbert systems... anything that lacks second-order instantiation of lemmas because you can just redo the lemma's proof in place. < 1582720818 94647 :arseniiv!~arseniiv@95.105.14.199.dynamic.ufanet.ru PRIVMSG #esoteric :cpressey: ah, hm, Metamath could be claimed to be an esoteric one, now that I think < 1582720832 156974 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(This is a first-order logic phenomenon, obviously. You prove something that holds for an arbitrary predicate P. But you can't instantiate P later on.) < 1582720866 760414 :arseniiv!~arseniiv@95.105.14.199.dynamic.ufanet.ru PRIVMSG #esoteric : anything that lacks second-order instantiation of lemmas because you can just redo the lemma's proof in place. => but that’s too boring, or should I say, inhumane < 1582721007 740357 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :If it's repetitive and inhumane in the way brainfuck code is repetitive and inhumane, that's an argument for it being esoteric < 1582721087 210107 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :And maybe one could build on that to make something a bit more interesting. < 1582721282 516495 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Yeah that was kind of my reasonings... those logics were not made to be used. < 1582721338 644160 :int-e!~noone@int-e.eu PRIVMSG #esoteric :They have their place in reasoning *about* proofs. (AKA Proof Theory.) < 1582721370 136691 :int-e!~noone@int-e.eu PRIVMSG #esoteric :So they're in a similar niche as (most) Turing tarpits. < 1582721421 849834 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(most, because some of them are really hard to reason about, and also some of them are actually fairly programmable...) < 1582721629 663259 :int-e!~noone@int-e.eu PRIVMSG #esoteric :The main programmable Turing tarpit is lambda calculus, simply because the mechanism for evaluation that is offers is very close to the mechanism we use for code reuse: take an existing paramterized program and instantiate the paramter. < 1582721699 579172 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Yes, basic data is represented in an unfamiliar way, but you can treat that as an abstraction... and soon you can write ordinary functional code. < 1582721833 274228 :rain1!~debian@unaffiliated/rain1 JOIN :#esoteric < 1582722925 679177 :kritixilithos!~kritixili@gateway/tor-sasl/kritixilithos JOIN :#esoteric < 1582724715 150756 :cpressey!~cpressey@5.133.242.4 PRIVMSG #esoteric :It does look like Coq is quite heavily used in the "proving properties of programming languages" space. < 1582724746 429269 :sprocklem!~sprocklem@unaffiliated/sprocklem QUIT :Ping timeout: 258 seconds < 1582724938 647860 :kritixil1!~kritixili@gateway/tor-sasl/kritixilithos JOIN :#esoteric < 1582725043 678139 :kritixilithos!~kritixili@gateway/tor-sasl/kritixilithos QUIT :Ping timeout: 240 seconds < 1582725092 670739 :kritixilithos!~kritixili@gateway/tor-sasl/kritixilithos JOIN :#esoteric < 1582725243 684311 :kritixil1!~kritixili@gateway/tor-sasl/kritixilithos QUIT :Ping timeout: 240 seconds < 1582725403 348768 :longname!~airbouy@75-26-238-119.lightspeed.glvwil.sbcglobal.net QUIT :Quit: Lost terminal < 1582725651 783509 :xkapastel!uid17782@gateway/web/irccloud.com/x-oolslzdmrjfvdmwr QUIT :Quit: Connection closed for inactivity < 1582725806 471857 :longname!~airbouy@75-26-238-119.lightspeed.glvwil.sbcglobal.net JOIN :#esoteric < 1582729123 674804 :kritixilithos!~kritixili@gateway/tor-sasl/kritixilithos QUIT :Ping timeout: 240 seconds < 1582729537 972101 :sprocklem!~sprocklem@unaffiliated/sprocklem JOIN :#esoteric < 1582730521 677491 :kritixilithos!~kritixili@gateway/tor-sasl/kritixilithos JOIN :#esoteric < 1582732332 157155 :Taneb!~Taneb@2001:41c8:51:10d:aaaa:0:aaaa:0 PRIVMSG #esoteric :`quote < 1582732335 94011 :HackEso!~h@unaffiliated/fizzie/bot/hackeso PRIVMSG #esoteric :764) Do you think " `addquote [with no context] < zzo38> Do you think psychology is worse, or not?" is worse, or not? < 1582732353 951330 :sprocklem!~sprocklem@unaffiliated/sprocklem QUIT :Ping timeout: 252 seconds < 1582732900 50007 :sprocklem!~sprocklem@unaffiliated/sprocklem JOIN :#esoteric < 1582733143 678252 :kritixilithos!~kritixili@gateway/tor-sasl/kritixilithos QUIT :Ping timeout: 240 seconds < 1582733259 920767 :cpressey!~cpressey@5.133.242.4 QUIT :Quit: A la prochaine. < 1582733611 675403 :kritixilithos!~kritixili@gateway/tor-sasl/kritixilithos JOIN :#esoteric < 1582735706 72920 :sprocklem!~sprocklem@unaffiliated/sprocklem QUIT :Ping timeout: 265 seconds < 1582736969 469150 :rain1!~debian@unaffiliated/rain1 QUIT :Quit: Lost terminal < 1582737312 677630 :kritixil1!~kritixili@gateway/tor-sasl/kritixilithos JOIN :#esoteric < 1582737342 385511 :arseniiv!~arseniiv@95.105.14.199.dynamic.ufanet.ru PRIVMSG #esoteric : If it's repetitive and inhumane in the way brainfuck code is repetitive and inhumane, that's an argument for it being esoteric => right, but that’s why I’m not writing in it and don’t make its analogs :D though I’m guilty in writing a simple interpreter of it, which compiles to a slightly optimized bytecode, but that was no big feat, so no special dedication too < 1582737403 677591 :kritixilithos!~kritixili@gateway/tor-sasl/kritixilithos QUIT :Ping timeout: 240 seconds < 1582737684 127120 :arseniiv!~arseniiv@95.105.14.199.dynamic.ufanet.ru PRIVMSG #esoteric :int-e: hmm now I think about a Hilbert-style language indeed, but with more usability still, though via adding a C-style preprocessor to it. Maybe that would be both simpler and a bit funny, as one would be able to write incorrect macros < 1582737797 573592 :arseniiv!~arseniiv@95.105.14.199.dynamic.ufanet.ru PRIVMSG #esoteric :hm could one continue the C analogy further?.. Like, how could we make a proof language not only just low-level, but also potentially unsafe?.. < 1582738331 251290 :arseniiv!~arseniiv@95.105.14.199.dynamic.ufanet.ru PRIVMSG #esoteric :eh, Metamath is very good at being esoteric in that way. One can write syntax definitions that would lead to ambiguity, and actual proofs in .mm files are stored as a RPN (if I remember that it’s a reverse one indeed) of rule applications, referenced by their names. And if that’s not enough unreadability, there’s also a compressed format (though fairly human-readable one, as it’s not a binary encoding of some sort, but a sequen < 1582738331 365899 :arseniiv!~arseniiv@95.105.14.199.dynamic.ufanet.ru PRIVMSG #esoteric :ce of rule names being used and then a string of corresponding ASCII letters (at least that’s what I’ve seen when there are not too many rules involved) < 1582738363 297266 :arseniiv!~arseniiv@95.105.14.199.dynamic.ufanet.ru PRIVMSG #esoteric :hard to outdo < 1582739117 689505 :tromp!~tromp@2a02:a210:ca3:2800:e571:85:fa78:c170 QUIT :Remote host closed the connection < 1582739671 949925 :tromp!~tromp@2a02:a210:ca3:2800:4999:1e25:9124:252d JOIN :#esoteric < 1582739821 561081 :kritixil1!~kritixili@gateway/tor-sasl/kritixilithos QUIT :Quit: quit < 1582740594 311238 :kspalaiologos!~kspalaiol@176.221.122.71 JOIN :#esoteric < 1582740610 670612 :kspalaiologos!~kspalaiol@176.221.122.71 PRIVMSG #esoteric :greets < 1582743284 458078 :kspalaiologos!~kspalaiol@176.221.122.71 QUIT :Quit: Leaving < 1582744067 305230 :LKoen!~LKoen@lstlambert-657-1-123-43.w92-154.abo.wanadoo.fr JOIN :#esoteric < 1582745758 750386 :Lord_of_Life_!~Lord@unaffiliated/lord-of-life/x-0885362 JOIN :#esoteric < 1582745857 241671 :Lord_of_Life!~Lord@unaffiliated/lord-of-life/x-0885362 QUIT :Ping timeout: 255 seconds < 1582745926 791553 :Lord_of_Life_!~Lord@unaffiliated/lord-of-life/x-0885362 NICK :Lord_of_Life < 1582747510 997211 :LKoen!~LKoen@lstlambert-657-1-123-43.w92-154.abo.wanadoo.fr QUIT :Remote host closed the connection < 1582747511 364069 :b_jonas!~x@catv-176-63-14-185.catv.broadband.hu JOIN :#esoteric < 1582748651 313973 :b_jonas!~x@catv-176-63-14-185.catv.broadband.hu PRIVMSG #esoteric :int-e: "finally" isn't that unusual, python and java and javascript and more languages also have that as a keyword < 1582749261 183890 :int-e!~noone@int-e.eu PRIVMSG #esoteric :b_jonas: that's totally missing the point < 1582749294 652082 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Isar's "finally" has a very different meaning. < 1582749298 273155 :rain1!~debian@unaffiliated/rain1 JOIN :#esoteric < 1582749772 278246 :zzo38!~zzo38@host-24-207-50-7.public.eastlink.ca PRIVMSG #esoteric :What is Isar's "finally" meaning? < 1582750123 319856 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Hrm. Isar is a proof language; the central statement is 'have "foo"' followed by a proof to establish that "foo" holds. Such facts can be used later one either by giving them names, or by chaining them more implicitly. < 1582750160 41105 :int-e!~noone@int-e.eu PRIVMSG #esoteric :One way of chaining is "then"; have "foo" then have "bar" makes "foo" available for the proof of "bar". < 1582750207 858443 :int-e!~noone@int-e.eu PRIVMSG #esoteric :But sometimes you want to chain multiple facts into a proof. You can do that using "moreover" and "ultimately": have "foo" moreover have "bar" ultimately have "baz" will chain "foo" and "bar" into the proof of "baz". < 1582750308 330572 :int-e!~noone@int-e.eu PRIVMSG #esoteric :Now... similar to "moreover" and "ultimately" there is another pair, "also" and "finally". They use transitive reasoning; if you do have "a = b" also have "b = c" finally have "foo" then the chained fact will be "a = c". (There's more to it; for example you can write "... = c" instead of "b = c", but this is the basic story.) < 1582750374 614345 :int-e!~noone@int-e.eu PRIVMSG #esoteric :The full gory details are somewhere in https://isabelle.in.tum.de/dist/Isabelle2019/doc/isar-ref.pdf < 1582750436 956565 :int-e!~noone@int-e.eu PRIVMSG #esoteric :(I also wonder whether any of that explanation made any sense.) < 1582751462 878405 :zzo38!~zzo38@host-24-207-50-7.public.eastlink.ca PRIVMSG #esoteric :Converting the German "ss" ligature into uppercase (e.g. "\xDF".toUpperCase()) produces "SS" in V8 JavaScript, but leaves it unchanged in Mozilla JavaScript. < 1582752446 456475 :b_jonas!~x@catv-176-63-14-185.catv.broadband.hu PRIVMSG #esoteric :int-e: wasn't the point that "moreover" and "ultimately" are strange words to be used as pl keywords? < 1582752601 721619 :b_jonas!~x@catv-176-63-14-185.catv.broadband.hu PRIVMSG #esoteric :maybe I only think that because I don't use SQL much < 1582753393 85676 :imode!~linear@unaffiliated/imode JOIN :#esoteric < 1582753908 718178 :rain1!~debian@unaffiliated/rain1 QUIT :Quit: Lost terminal < 1582754029 152940 :b_jonas!~x@catv-176-63-14-185.catv.broadband.hu PRIVMSG #esoteric :ah, I see arseniiv already said that about "finally" < 1582754295 451762 :arseniiv!~arseniiv@95.105.14.199.dynamic.ufanet.ru PRIVMSG #esoteric : (I also wonder whether any of that explanation made any sense.) => I don’t know how proofs look like but I think I get these constructs in most part < 1582758462 93694 :LKoen!~LKoen@81.255.219.130 JOIN :#esoteric < 1582759840 821975 :LKoen!~LKoen@81.255.219.130 QUIT :Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.” < 1582760194 184610 :imode!~linear@unaffiliated/imode QUIT :Ping timeout: 255 seconds