3 ms·
Hardly. How often is it that you can read an uncommented Python program that implements a tricky algorithm, and you can easily recover basic things like loop in
by catnaroek 10y ago
Hardly. How often is it that you can read an uncommented Python program that implements a tricky algorithm, and you can easily recover basic things like loop invariants?
- yorwba 10y agoFor that you'd really want something like Dafny https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/ https://www.microsoft.com/en-us/research/project/dafny-a-lan... where your program doesn't even compile if you don't give it the right invariant.
- catnaroek 10y agoBut then there's no such thing as an unannotated program. I'm confident in my ability to prove things the old-fashioned way, using brain, pencil and paper, so I don't see much value in merely having my proofs verified by a machine. If the machine can't contribute to the effort of actually coming up with the proof, it should stay out of the way.