The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

I do think it's worth drawing a distinction between the mathematician's 
goal of understanding a proof to attain "insight" (honestly driven 
primarily by aesthetic criteria in many cases, as far as I can tell) and 
the formal-methods engineer's goal of understanding a proof to be able 
to maintain it.  We measure success very differently in these two cases, 
I would claim.  Insight can be a tool to put a person in a good position 
to do maintenance, but good enough automation can remove the need to 
develop any insight about many details in a long proof.

On 1/12/20 11:45 AM, Stefan Monnier wrote:
> > 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.