The Coq mailing list

[Alan Pogrebinschi <alanpog AT gmail.com>]

I'm just starting with Coq, and I'm intrigued by how little structured
proofs seem to be used here, as you say. Declarative proofs, in
principle, should be much easier to read and maintain (not necessarily
to write). And in other systems, like Isabelle, they seem to have a
wider adoption (they had it for a longer time too).
I'm curious about the reasons you wouldn't recommend using it. Is it
just the state of the current implementation in Coq the problem?
Thanks,
Alan

On Fri, Nov 11, 2011 at 8:28 PM, Adam Chlipala 
<adamc AT csail.mit.edu>
 wrote:
> A brief note, and someone should correct me if I'm wrong about this: I
> believe the user base of "structured proofs" in Coq is negligible.  Few of
> us here have any experience with it or recommend using it.
>