The Coq mailing list

[Stefan Monnier <monnier AT iro.umontreal.ca>]

> This is why I do not really care if Coq (or lean or agda or anything
> else's) proofs are readable or not when it comes to program verification.

As a user of the program, that makes sense.  But if you ever intend to
work (extend, modify, ...) on that program (or pay someone else to do
it), then you'll need this proof to be readable, just like you need the
code to be readable, otherwise you won't be able to update the proof to
match the new code.


        Stefan