This is the web site for the early stages of a book introducing both machine-checked proof with the Coq proof assistant and approaches to formal reasoning about program correctness.