CoqAn 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 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.
Nota bene: 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