
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 _(tactic)s (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 class="comment">NOTE: This is by all observations a heavy influence on _(Fare)'s early thinking and writing about the _(TUNES Project), so reading it will help those without his experience understand his use of technical terms a little better.--_(water)</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>