The Coq mailing list

[Wouter Swierstra <wss AT cs.nott.ac.uk>]

> On the issue of proofs, I think the proof scripts in both your (Adam  
> Koprowski's) code and the code of the mysterious "muad" are manual  
> enough that I would refuse to accept them in a serious  
> development. ;-)  I say that every certified function should have a  
> single proof script associated with it, and that proof script should  
> be a single tactic, with no intermediate periods.  That style (which  
> I used in my implementation posted earlier) is easy to use when you  
> commit to following it, and it has many advantages in brevity of  
> code and resilience to changes in specs and implementations.

That's a very interesting point. I certainly agree that proof scripts  
can extremely brittle (especially if their poorly engineered) - but  
aren't you just moving the problem somewhere else? You have a lot more  
experience with this than I do, but why are Ltacs any easier to  
maintain than proof scripts?

  Wouter