The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Hugo Herbelin wrote:
> > You are proving a theorem whose type belongs to [Prop].  That means the 
> > proof really is a proof, and every proof is equivalent computationally.  
> > There is never any reason to prefer any proof to another, putting aside 
> > issues of how difficult different proof strategies are to code.
> >     
>
> I would not be so peremptory. If the common view is indeed to "think"
> proofs as computationally irrelevant, this is not enforced by the
> logic of Coq and "proof-relevant" models remain available. Moreover,
> even if a logic is proof-irrelevant, this does not mean that the
> computational content of the proofs cannot be observed and
> manipulated at the meta-level. See e.g. Alexandre Miquel's
> realizability and extraction for Prop which supports classical
> reasoning and, even, proof-irrelevance (at the logical level).
>   

Still, I believe that, for someone _new_ to Coq and not interested in 
pondering metatheory, thinking about [Prop] non-irrelevantly is most 
likely to lead only to misleading intuitions.  There is a substantial 
amount of talk out there about "extracting programs from proofs," and I 
feel that a lot of newcomers to Coq end up confused because they assume 
that this is how Coq is usually used.

> In any case, let's keep this list friendly!
>   

OK, I feel I need to step in briefly to make one thing clear, since I 
don't want the reputation of a crotchety ogre who breakfasts on the 
bones of newbies: I see no point during this thread where anyone was 
unfriendly.  I think we have an issue of miscommunication across 
cultures and conventions of expression.  I'm going to try to learn from 
this to avoid writing things that bother people in the future, but I 
hope you can take my word for it that I wasn't trying to be anything but 
friendly and helpful at any point.