Coq
An 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.
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
This page is linked from: Quotienting Tactic