The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

Hi,

> 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).

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

Hugo Herbelin