Jon Sterling5d 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 Sterling5d 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. Allais5d ago
@jonmsterling what we need is a week (more?) long summer school on implementing something that's not a toy.
Show threadJesper Agdakx 🔸4d ago
@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.
Show threadJon Sterling
@jesper @gallais I love the idea... but I can't imagine being away from my job (teaching!) or my wife for a whole semester.
Mar 25 at 10:35amWeb