[Ericson2314]

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]

Reminds 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