4 ms·
This was a nice read. It was especially nice for the authors to say many times things like "we had _x_ trouble with Lean but it didn't feel like Lean's fault".
by Ericson2314 1y ago
This was a nice read. It was especially nice for the authors to say many times things like "we had _x_ trouble with Lean but it didn't feel like Lean's fault". That feels new to me!
- readthenotes1 1y agoReminds me of an early attempt at a language created to prove program correctness. One attempt reported there were more errors in the proving language than in the program itself