<p>This is the web site for an in-progress textbook about practical engineering with <ahref="http://coq.inria.fr/">the Coq proof assistant</a>. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation.</p>