The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

muad wrote:
> > and the code of the mysterious "muad" are manual 
> > enough that I would refuse to accept them in a serious development. ;-)  
> >     
>
> Nobody would accept such an algorithm in serious development having O(n^2)
> complexity, the purpose is to show a beginner how to interactively define a
> program with correctness proof.
>   

You seem to be assuming that automation is an "advanced" topic.  In my 
view, the situation is exactly the opposite.  Beginners should be doing 
100% automated proofs for their first month of Coq usage, at least, and 
that's why I took the trouble of including some power-tactics for that 
purpose in my book.

Most computer scientists aren't willing to work with manual proofs, 
period, and that's not just because they like to make trouble for 
interactive proof assistant people.