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?
2020-12-02 21:14:37 +0100 <geekosaur> not sure I have ops here but can try
2020-12-02 21:14:45 +0100 <geekosaur> (not sure anyone has ops here any more)
2020-12-02 21:15:21 +0100 <geekosaur> right, no ops
2020-12-02 21:15:37 +0100 <Liskni_si> well dons is active on Twitter and last time I asked him about xmonad, he replied quickly that he's still a user so he'd probably be able to transfer access
2020-12-02 21:15:52 +0100 <Liskni_si> (might as well ask him for adding mods to /r/xmonad)
2020-12-02 21:17:04 +0100 <geekosaur> oh, there are newer people with acess, but they keep disappearing too
2020-12-02 21:17:52 +0100 <Liskni_si> maybe byorgey has access?
2020-12-02 21:19:04 +0100 <geekosaur> nope
2020-12-02 21:19:21 +0100 <geekosaur> /msg chanserv access #xmonad list
2020-12-02 21:19:22 +0100 <tomsmeding> the current topic is set by them, however
2020-12-02 21:19:38 +0100 <geekosaur> but I haven't seen any of them in some time
2020-12-02 21:23:37 +0100 <Liskni_si> we can send them an e-mail :-)
2020-12-02 21:23:55 +0100 <geekosaur> gwern's around, I'm asking for help
2020-12-02 21:23:57 +0100gwern(~gwern@wikipedia/Gwern)
2020-12-02 21:24:51 +0100ChanServ+o gwern
2020-12-02 21:25:35 +0100ChanServ+o geekosaur
2020-12-02 21:26:03 +0100 <geekosaur> thanks
2020-12-02 21:26:48 +0100gwern+o geekosaur
2020-12-02 21:27:39 +0100 <gwern> I assume no one has any objections to geekosaur being added to ops?
2020-12-02 21:27:53 +0100 Want to help? http://bit.ly/2nYjqpQ | xmonad: the tiling window manager with formally proven extensions | http://xmonad.org | http://xmonad.org/faq | cheatsheet: http://bit.ly/gz1R4 | https://ircbrowse.tomsmeding.com/browse/xmonad
2020-12-02 21:28:01 +0100 <geekosaur> everyone thought I already had ops
2020-12-02 21:28:28 +0100 <Liskni_si> ^^ :-)
2020-12-02 21:29:07 +0100geekosaur-o geekosaur
2020-12-02 21:39:23 +0100doct0rhu(~orctarorg@pool-72-88-158-154.nwrknj.fios.verizon.net)
2020-12-02 21:52:39 +0100ChubaDuba(~ChubaDuba@5.167.119.188)