By Adam Chlipala,
http://adam.chlipala.net/cpdt/
This is the web site for an in-progress textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation.