The Coq mailing list

[Nadeem Abdul Hamid <nadeem AT acm.org>]

Adam,

> >  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?

(I have downloaded your book but not gone through it yet.) I have  
found Ltacs hard to develop because it's difficult to debug them, more  
so than a broken proof script. If a complex tactic defined with Ltac  
doesn't succeed on a goal, I don't recall that the error messages are  
very helpful for tracking down what happened.

--- nadeem