00:50:30 <zzo38> 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.
00:50:32 <zzo38> 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).
00:53:03 -!- imode has joined.
01:07:09 <zzo38> Do you like this?
01:12:22 -!- FreeFull has quit.
01:25:45 <b_jonas> zzo38: ooh, that part about the tree and desert sounds like Jimmy Knopf
01:26:52 <zzo38> Who is Jimmy Knopf?
02:31:41 -!- oerjan has joined.
02:39:18 <oerjan> the birth of ennesquid
02:39:26 <oerjan> </spoiler>
02:49:53 <zzo38> What is that?
02:50:50 <oerjan> latest schlock mercenary
03:03:16 <oerjan> `olist 1193
03:03:18 <HackEso> olist 1193: shachaf oerjan Sgeo FireFly boily nortti b_jonas
03:16:12 <oerjan> @metar ENVA
03:16:12 <lambdabot> ENVA 260250Z 12006KT CAVOK M11/M13 Q0998 RMK WIND 670FT 10009KT
03:23:22 -!- imode has quit (Ping timeout: 255 seconds).
04:20:06 <zzo38> 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.
04:31:24 -!- xkapastel has joined.
05:03:34 -!- imode has joined.
05:44:43 -!- xelxebar has quit (Remote host closed the connection).
05:46:43 -!- xelxebar has joined.
06:05:51 -!- arseniiv has joined.
06:08:52 -!- xelxebar has quit (Remote host closed the connection).
06:09:16 -!- Sgeo_ has quit (Read error: Connection reset by peer).
06:09:42 -!- Sgeo_ has joined.
06:33:29 <arseniiv> `? password
06:33:31 <HackEso> The password of the month is leapfrogging rats.
06:34:52 <arseniiv> leap earring
06:35:46 <arseniiv> it would be silly and wonderful if we didn’t know if the current year is leap until it almost ends
06:36:12 <arseniiv> with the mechanism like something with leap seconds, I presume?
07:04:50 -!- imode has quit (Ping timeout: 240 seconds).
07:24:11 -!- ArthurStrong has joined.
07:26:08 -!- xelxebar has joined.
07:28:43 -!- xelxebar has quit (Remote host closed the connection).
07:29:10 -!- xelxebar has joined.
07:36:20 -!- Lord_of_Life_ has joined.
07:36:59 -!- Lord_of_Life has quit (Ping timeout: 272 seconds).
07:37:40 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
07:48:47 <esowiki> [[User talk:Oklomsy]]  https://esolangs.org/w/index.php?diff=70054&oldid=68946 * Oklomsy * (+125) /* New language idea maybe. */ new section
07:49:26 <esowiki> [[User talk:Oklomsy]]  https://esolangs.org/w/index.php?diff=70055&oldid=70054 * Oklomsy * (+66) /* New language idea maybe. */
08:27:19 <int-e> fungot: what's my motivation?
08:27:20 <fungot> int-e: you mean demoscene.tv requires proprietary software? :) fnord/ compilers/ linguine/ linguine.py': errno 13 permission denied: ' lament'
08:28:15 <oerjan> the proprietary fnord suite, the bane of demosceners everywhere
08:31:41 -!- ArthurStrong has quit (Quit: leaving).
08:32:40 <int-e> Freefall isn't helping my motivation either.
08:32:56 <int-e> (Monday's that is)
08:34:06 <oerjan> 's ok sam will fix it all he just needs to get a green cloak for proper style
08:34:53 <oerjan> s/cloak/outfit/
08:35:38 <oerjan> today's girl genius went about as i'd expected
08:35:54 <oerjan> (vaguely)
08:36:14 <int-e> Nice reminder of the hat though.
08:37:21 <oerjan> there were way too many scenes in comic where gil _should_ have noticed.
08:40:18 <int-e> But Gil never notices anything, except when it matters.
08:40:56 <oerjan> i'm pretty sure it's been pointed out that he notices more than he lots on
08:41:11 <oerjan> *lets
08:42:07 <int-e> Not that I noticed ;)
08:43:11 <int-e> (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.)
08:59:24 -!- b_jonas has quit (Quit: leaving).
09:17:01 -!- cpressey has joined.
09:20:51 -!- xkapastel has quit (Quit: Connection closed for inactivity).
09:20:52 <cpressey> int-e: Now that your paper is safely submitted to AFP, I could give you my feedback.
09:22:08 <int-e> cpressey: I might feel obliged to update it...
09:23:01 <int-e> (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.)
09:23:17 <int-e> The old versions are archived, so it's still transparent.
09:23:28 <int-e> cpressey: But sure, go ahead if you like.
09:31:17 <cpressey> "omg in Isabelle/HOL the expression for G_16 cannot be typed?! lol l/\m3"
09:31:25 <cpressey> See, I didn't think you'd find it useful.
09:33:38 <int-e> 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.
09:34:30 <int-e> (Or figure out whether there should be more ITPs or programming languages on that list.)
09:45:22 <cpressey> 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.
09:45:46 -!- longname has quit (Read error: Connection reset by peer).
09:46:00 <cpressey> I am tickled by the fact that Isabelle has "moreover" and "ultimately" keywords.
09:48:16 <int-e> cpressey: It also has 'also' and 'finally'.
09:48:29 -!- longname has joined.
09:48:30 <int-e> cpressey: Which are for chaing (in)equalities.
09:48:47 <int-e> *chaining* (is that an auto-portmonteau?)
09:52:54 <cpressey> int-e: Have you seen https://github.com/avigad/arwm ?  I found the slides interesting, haven't read the notes yet.
09:55:27 <int-e> No I have not.
09:55:56 <int-e> August 2019, hmm.
10:00:58 <int-e> Well, not sure how I could've found out either; for example, I don't see anything on the isabelle users mailing list...
10:01:09 <int-e> (though perhaps I missed it)
10:10:36 -!- xkapastel has joined.
10:15:11 <cpressey> Gah, looking over all the choices again, I still can't decide, and I forget why I wanted to do this again?
10:22:09 <int-e> 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).
10:23:15 <int-e> (One of the running gags is that formalizing a paper proof is easy until you run into the word "obviously".)
10:27:15 <int-e> 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...
10:27:21 <int-e> ...out. Agda is more of a programming language. I'm sure I'm missing a ton of other stuff.
10:31:17 <int-e> 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.
10:34:35 <int-e> 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).
10:34:49 <int-e> (And of course because I've used it way more than Coq.)
10:40:34 <int-e> 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...
10:40:40 <int-e> ...it out)
10:42:02 <int-e> 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.
10:42:56 <int-e> 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.
10:45:41 <int-e> (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...
10:45:47 <int-e> ...extracting those hints for auto from that).
10:47:10 <int-e> Hmm, long monologue. Oh well, this is about 6 years of my life.
10:51:08 <cpressey> int-e: Thank you. I was in fact leaning towards Coq (yesterday, before I started wondering why I wanted to do this again).
10:57:35 <cpressey> 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.
10:57:58 <cpressey> I tried to learn Agda once. It didn't go well.
10:58:11 <int-e> 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...
10:58:17 <int-e> ...experience with Isabelle/HOL. I still think that Coq is a tad worse at arithmetic (which does come up a few times).
11:00:16 <cpressey> 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.
11:00:42 <int-e> (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...
11:00:48 <int-e> ...https://en.wikipedia.org/wiki/Dilworth%27s_theorem#Inductive_proof .
11:01:20 <int-e> cpressey: Oh I'm not a huge fan of dependent types either *especially* for programming.
11:02:48 <int-e> 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.
11:03:22 <int-e> ("trust me, I know that n+m = m+n for natural numbers")
11:03:38 <Taneb> I like dependent types but mostly because I find them fun
11:03:56 <int-e> I'm less dismissive of their use in ITPs though.
11:04:16 <int-e> Since there the purpose is to prove everything rigorously.
11:05:26 <int-e> 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.)
11:05:26 <Taneb> 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?
11:05:52 <int-e> Taneb: That's the kind of thing I'm after, yes. Except that's too verbose.
11:08:10 <int-e> 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.
11:08:19 <Taneb> 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
11:08:50 <int-e> Taneb: <int-e> I've been meaning to look at Lean for a while now.
11:09:12 <Taneb> Ah, I didn't see that
11:09:13 <int-e> (No, I can't really blame you for not reading all that.)
11:09:46 <int-e> (Especially since I am terrible at catching up on context myself.)
11:15:36 -!- oerjan has quit (Quit: Nite).
11:15:37 <cpressey> 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.
11:16:54 <cpressey> 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?
11:17:21 <cpressey> Like (just blue-skying here) System F, or System F_omega?
11:18:02 <cpressey> (Or do you just get a programming language if you try that?)
11:19:00 <Taneb> I keep meaning to mess around more with metamath
11:20:12 <int-e> 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"...
11:20:56 <int-e> (But as usual this may be my lack of imagination.)
11:23:57 <cpressey> It could come from the burgeoning field of esoteric proof languages... :)
11:24:09 <cpressey> Or it could if I had more spare time
11:25:01 <int-e> Well, making a /usable/ ITP is a huge effort.
11:25:12 <cpressey> No argument there
11:34:41 <cpressey> 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.)
11:35:28 <cpressey> And realized that conventional exception handling is (roughly speaking) dynamically scoped and therefore technically violates referential transparency.
12:19:51 <arseniiv> <cpressey> I am tickled by the fact that Isabelle has "moreover" and "ultimately" keywords. <int-e> cpressey: It also has 'also' and 'finally'. => wow! Though, `finally` isn’t that new after languages with C-like syntax and exceptions
12:22:08 <int-e> arseniiv: Well, it doesn't have "throw".
12:24:22 <arseniiv> int-e: I propose adding “throw” somewhere as a comment marker, like in “throw that human language text away” :D
12:26:03 -!- iczero has quit (Excess Flood).
12:26:07 -!- Bowserinator has quit (Ping timeout: 252 seconds).
12:26:23 -!- iczero has joined.
12:26:27 <arseniiv> 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)
12:26:39 -!- Bowserinator has joined.
12:33:11 <int-e> arseniiv: can you name a non-esoteric one...
12:34:08 <arseniiv> int-e: erm, don’t Isabelle, Coq, Agda mentioned above count?
12:35:30 <cpressey> I have https://github.com/catseye/Maxixe but it's hardly esoteric.
12:35:45 <cpressey> Metamath's syntax certainly *looks* esoteric.
12:37:38 <int-e> arseniiv: I may have been somewhat facetious there. :P
12:39:28 <int-e> 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.
12:40:18 <arseniiv> cpressey: ah, hm, Metamath could be claimed to be an esoteric one, now that I think
12:40:32 <int-e> (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.)
12:41:06 <arseniiv> <int-e> 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
12:43:27 <cpressey> If it's repetitive and inhumane in the way brainfuck code is repetitive and inhumane, that's an argument for it being esoteric
12:44:47 <cpressey> And maybe one could build on that to make something a bit more interesting.
12:48:02 <int-e> Yeah that was kind of my reasonings... those logics were not made to be used.
12:48:58 <int-e> They have their place in reasoning *about* proofs. (AKA Proof Theory.)
12:49:30 <int-e> So they're in a similar niche as (most) Turing tarpits.
12:50:21 <int-e> (most, because some of them are really hard to reason about, and also some of them are actually fairly programmable...)
12:53:49 <int-e> 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.
12:54:59 <int-e> 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.
12:57:13 -!- rain1 has joined.
13:15:25 -!- kritixilithos has joined.
13:45:15 <cpressey> It does look like Coq is quite heavily used in the "proving properties of programming languages" space.
13:45:46 -!- sprocklem has quit (Ping timeout: 258 seconds).
13:48:58 -!- kritixil1 has joined.
13:50:43 -!- kritixilithos has quit (Ping timeout: 240 seconds).
13:51:32 -!- kritixilithos has joined.
13:54:03 -!- kritixil1 has quit (Ping timeout: 240 seconds).
13:56:43 -!- longname has quit (Quit: Lost terminal).
14:00:51 -!- xkapastel has quit (Quit: Connection closed for inactivity).
14:03:26 -!- longname has joined.
14:58:43 -!- kritixilithos has quit (Ping timeout: 240 seconds).
15:05:37 -!- sprocklem has joined.
15:22:01 -!- kritixilithos has joined.
15:52:12 <Taneb> `quote
15:52:15 <HackEso> 764) <zzo38> Do you think " `addquote [with no context] < zzo38> Do you think psychology is worse, or not?" is worse, or not?
15:52:33 -!- sprocklem has quit (Ping timeout: 252 seconds).
16:01:40 -!- sprocklem has joined.
16:05:43 -!- kritixilithos has quit (Ping timeout: 240 seconds).
16:07:39 -!- cpressey has quit (Quit: A la prochaine.).
16:13:31 -!- kritixilithos has joined.
16:48:26 -!- sprocklem has quit (Ping timeout: 265 seconds).
17:09:29 -!- rain1 has quit (Quit: Lost terminal).
17:15:12 -!- kritixil1 has joined.
17:15:42 <arseniiv> <cpressey> 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
17:16:43 -!- kritixilithos has quit (Ping timeout: 240 seconds).
17:21:24 <arseniiv> 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
17:23:17 <arseniiv> 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?..
17:32:11 <arseniiv> 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
17:32:11 <arseniiv> 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)
17:32:43 <arseniiv> hard to outdo
17:45:17 -!- tromp has quit (Remote host closed the connection).
17:54:31 -!- tromp has joined.
17:57:01 -!- kritixil1 has quit (Quit: quit).
18:09:54 -!- kspalaiologos has joined.
18:10:10 <kspalaiologos> greets
18:54:44 -!- kspalaiologos has quit (Quit: Leaving).
19:07:47 -!- LKoen has joined.
19:35:58 -!- Lord_of_Life_ has joined.
19:37:37 -!- Lord_of_Life has quit (Ping timeout: 255 seconds).
19:38:46 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
20:05:10 -!- LKoen has quit (Remote host closed the connection).
20:05:11 -!- b_jonas has joined.
20:24:11 <b_jonas> int-e: "finally" isn't that unusual, python and java and javascript and more languages also have that as a keyword
20:34:21 <int-e> b_jonas: that's totally missing the point
20:34:54 <int-e> Isar's "finally" has a very different meaning.
20:34:58 -!- rain1 has joined.
20:42:52 <zzo38> What is Isar's "finally" meaning?
20:48:43 <int-e> 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.
20:49:20 <int-e> One way of chaining is "then"; have "foo" <proof> then have "bar" <proof> makes "foo" available for the proof of "bar".
20:50:07 <int-e> But sometimes you want to chain multiple facts into a proof. You can do that using "moreover" and "ultimately": have "foo" <proof> moreover have "bar" <proof> ultimately have "baz" <proof> will chain "foo" and "bar" into the proof of "baz".
20:51:48 <int-e> Now... similar to "moreover" and "ultimately" there is another pair, "also" and "finally". They use transitive reasoning; if you do  have "a = b" <proof> also have "b = c" <proof> finally have "foo" <proof> 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.)
20:52:54 <int-e> The full gory details are somewhere in https://isabelle.in.tum.de/dist/Isabelle2019/doc/isar-ref.pdf
20:53:56 <int-e> (I also wonder whether any of that explanation made any sense.)
21:11:02 <zzo38> Converting the German "ss" ligature into uppercase (e.g. "\xDF".toUpperCase()) produces "SS" in V8 JavaScript, but leaves it unchanged in Mozilla JavaScript.
21:27:26 <b_jonas> int-e: wasn't the point that "moreover" and "ultimately" are strange words to be used as pl keywords?
21:30:01 <b_jonas> maybe I only think that because I don't use SQL much
21:43:13 -!- imode has joined.
21:51:48 -!- rain1 has quit (Quit: Lost terminal).
21:53:49 <b_jonas> ah, I see arseniiv already said that about "finally"
21:58:15 <arseniiv> <int-e> (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
23:07:42 -!- LKoen has joined.
23:30:40 -!- LKoen has 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.”).
23:36:34 -!- imode has quit (Ping timeout: 255 seconds).