<P>
Coq is a higher-order proof system based on the _(Curry-Howard isomorphism) between propositions and types, proofs and terms in a pure *(functional) *(programming language): a functional term is a proof of its type's realizability. By restraining to constructive intuitionistic logic (i.e. no built-in choice axiom), it allows extraction of actual programs from proofs.

The newer version of Coq does have programmable tactics (using _(Ocaml)),
extensible grammars, etc.

The problem with Coq is that it is not reflective: there is a one global
meta-context, and no way to meta-translate expressions: a proof done in
"Prop" will have to be done again in "Set" and in "Type" as there are no
"proof sketches" as first-class objects.
</P>
<UL CLASS="links">
<LI><A HREF="http://pauillac.inria.fr/coq/">WWW Site</A></LI>
<LI><A HREF="ftp://ftp.inria.fr/local/coq/">FTP Site</A></LI>
</UL>