The Coq mailing list

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

John Nicol wrote:
> Thanks for the info!  Reading through the thread, it does sound like
> Czar is not supported enough for serious usage.  That's too bad -- I
> was hoping that would be the future path of Coq.
>
> [...]
> Oh well.  I guess the lesson for me is that the current systems still
> aren't ready for me (or I'm not ready for them :-) ).  Thanks for your
> time.  I'll continue to watch Coq's progress.
>   

I've resisted jumping in until now, but I think it's worth pointing out 
that some of us are very skeptical that declarative proofs are a good 
idea.  The style of imperative Coq proof that you see in the wild is not 
the only other option.  My book CPDT presents another style which I 
believe dominates both the common Ltac style and the declarative style 
(in any proof assistant) for ease of writing, reading, and maintaining 
proofs:
   http://adam.chlipala.net/cpdt/