Automated proofs and Coq

I ... need more sleep before really understanding what Coq can do, but apparently it's a theorem proving assistant, by which I understand it to be a system that can check your proofs for consistency if you stick to a machine-readable format for describing them.  I guess?

• Certified programming using it (a new book)
• A worked example of a stack machine compiler
• The Fundamental Theorem of Algebra.  No, really.