Jon Sterling4d ago

I think my code suffered from a kind of subtle version of the “Goodbye, Lenin” problem — which was hard to tell since I have never run it 🫠🤣

But yesterday I took some time to rearchitect things and I believe I have forestalled any possible version of this. Famous last words, etc., etc.

I’ve also (I believe!) corrected my implementation of observational postponement, which had been way too naïve and wasn’t stable under weakening.

Show threadJon Sterling4d ago
Implementing proof assistants is really arcane, isn’t it? If I were reading this post as someone inexperienced in this area I would think it was gobbledygook.
Show threadG. Allais4d ago
@jonmsterling what we need is a week (more?) long summer school on implementing something that's not a toy.
Show threadJesper Agdakx 🔸
@gallais @jonmsterling or a whole special semester bringing together all the experts so they can figure out both all the good ways to implement one and perhaps even write a book on it.
Mar 25 at 10:28amWeb
Show threadJon Sterling4d ago
@jesper @gallais I love the idea... but I can't imagine being away from my job (teaching!) or my wife for a whole semester.
Show threadMeven Lennon-Bertrand4d ago
@jesper @gallais @jonmsterling This would be extremely cool!
Show threadJan de Muijnck-Hughes4d ago

@mevenlennonbertrand @jesper @gallais @jonmsterling not cool but Dagsthul…

Although, iiuc, it’s not the kind of thing Daghtul is for. But Scotland could lead forwards with an FP Castle sort of gig….