Note: This channel on freenode is currently not being logged anymore. The logs are reproduced here for posterity.

2020-12-02 20:54:53 +0100ircbrowse_tom(~ircbrowse@64.225.78.177)
2020-12-02 20:54:53 +0100Server+cnt
2020-12-02 20:55:35 +0100 <tomsmeding> https://ircbrowse.tomsmeding.com/browse/xmonad
2020-12-02 20:55:50 +0100 <tomsmeding> looks like znc's config pages work fine with lynx :)
2020-12-02 20:56:09 +0100 <geekosaur> thank you
2020-12-02 20:56:19 +0100 <mc47> thanks!
2020-12-02 21:00:40 +0100 <Solid> awesome, thank you so much :)
2020-12-02 21:03:05 +0100 <tomsmeding> no problem :)
2020-12-02 21:03:18 +0100 <tomsmeding> Let me ask a question in return: the topic says "... with formally proven extensions"
2020-12-02 21:03:46 +0100 <tomsmeding> is that an exaggeration or is the behaviour/correctness/non-crashyness? of extensions really formally proven?
2020-12-02 21:04:24 +0100 <mc47> Some parts of the core have been formalized in Coq and formally proven
2020-12-02 21:04:27 +0100 <mc47> https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.722.3692&rep=rep1&type=pdf
2020-12-02 21:05:02 +0100 <Solid> I think there are some proofs for some extensions around
2020-12-02 21:05:04 +0100 <geekosaur> and someone did do a subset of the extensions at one point
2020-12-02 21:05:07 +0100 <Solid> but the stackset is certainly the most impressive
2020-12-02 21:05:37 +0100 <tomsmeding> cool!
2020-12-02 21:05:38 +0100 <geekosaur> but only a subset because some require X11 types, whereas the Coq proofs used basic types in their place
2020-12-02 21:06:14 +0100 <geekosaur> there's a reason e.g. StackSet has 5 type parameters, it's specifically to support this by letting the X11 types be swapped for things modelable in Coq
2020-12-02 21:06:47 +0100 <tomsmeding> and formally verifying X11 is not something that a sane person wants to do :)
2020-12-02 21:06:58 +0100 <geekosaur> none of this is recent, but xmonad's core in particular doesn't change often
2020-12-02 21:07:26 +0100 <tomsmeding> oh hey that paper is written by someone from the university where I'm studying :)
2020-12-02 21:07:43 +0100 <tomsmeding> in fact had a class from them
2020-12-02 21:08:56 +0100 <mc47> When I mentioned "XMonad have been forrmalized in Coq" in the presentation, the supervisors looked at me funny because they're maintaining/working with Isabelle/HOL
2020-12-02 21:14:09 +0100 <Solid> hah
2020-12-02 21:14:19 +0100 <Liskni_si> geekosaur: can you put https://ircbrowse.tomsmeding.com/browse/xmonad in the topic pls?