is a fashionable proof assistant...something I've been reading up on lately.
One family of proof assistants are "declarative": you write in a human-readable manner, so even if I don't have the program...I can read your code and see if it makes sense.
The other family is "procedural": you have tactics (which apply formal rules of transformation on the goal), then apply one after another. This is not too human readable, but works well with higher order logic...at least, that's my understanding.
Coq belongs to the former. I don't really see why I should get anymore excited about Coq than I should about, say, HOL. Well, Coq uses a synthesis of Martin-Lof type theory fused with a variant of the F# corner of the Lambda cube for its type theory (the so-called "Calculus of Inductive Constructions"), whereas HOL uses classical Higher Order Logic.
Every term in HOL appears to be a "thm" type, so proofs are literally the construction of objects.
The only point for Coq is its tactics are more "intuitive"...so while unreadable, it's not as
unreadable as HOL. Hmm...http://www.cis.upenn.edu/~bcpierce/sf/current/index.html