The Coq mailing list

["Klaus Ostermann" <ostermann AT informatik.tu-darmstadt.de>]

Hi all,

I am new to Coq (and theorem proving) and have a few (probably trivial)
questions that I have not found in the FAQ or elsewhere:

1) What is the technical difference between Prop and Set? The tutorial and
the book contain a few paragraphs that look like "philosophical" differences
(e.g., regarding proof irrelevance), but is there also a technical
difference? I.e., a situation where I can only use Prop but not Set or vice
versa.

2) I am quite fascinated by the fact that Coq turns every proof into a
program or function, but I wonder what these functions are good for, except
for proving other theorems. Is there a "use case" where I have a
constructive proof of a theorem that is then later used to extract code that
is executed?

3) If I import the law of excluded middle and use it, Coq can still generate
a function for each proof. How is this possible? I thought the Curry-Howard
isomorphism breaks down then because such proofs were not constructive?

4) What sets Coq apart from other proof assistants such as Isabelle/HOL?
Probably the most significant difference is that Coq is based on the
calculus of constructions, right? But what does this imply for a user? What
can I do with Coq that I cannot do (easily) with Isabelle? What is Coq bad
at?