Chlipala’s text is an outstanding introduction to how programs can be guaranteed to be correct by means of the Coq theorem prover, programs that are, in his terminology, “certified.” While machine-assisted proof has been possible for more than a quarter of a century, it is only in the last five years that a substantial body of fully formal proofs has been delivered. These include mathematical results, such as Gonthier’s proof of the four-color theorem, and also those in the domain of theoretical computer science. Indeed, the POPLmark challenge [1] has set a benchmark for proof mechanization in language metatheory. So, this text is timely in providing an accessible introduction to the area, but what is it that makes it stand out?

First, Chlipala gives an excellent introduction to the area, explaining the background of the different approaches to theorem proving in systems such as ACL2 and PVS among others, as well as the Coq system, which is the subject of the book. Complementing this is a discussion of the logics implemented by the various systems. He argues cogently for a theory that supports dependent types, under which the resulting types of functions can depend upon the values of inputs. Dependently typed systems support a dual interpretation: objects can be seen as values belonging to types, or equivalently as proofs for propositions, the so-called Curry-Howard isomorphism.

Allowing the interpretations to coexist yields a type system that can express program preconditions, or alternatively a logic in which a functional programming language can be used to build proofs. Coq implements a powerful dependently typed theory that has a functional programming foundation, proof checking in a secure kernel (according to the de Bruijn principle), advanced proof automation through a tactic language (Ltac), and a principle of reflection.

Second, Chlipala opens the exposition in chapter 2 with a worked set of examples that concentrate on language evaluators and compilers. Rather than covering all of the material needed first, he plunges into the exposition, giving a survey of what is possible, and saying that “it is expected that most readers will not understand what exactly is going on here.” Does this approach work? It is clear that anyone reading the chapter needs to understand a language like Haskell or ML. With that knowledge, it is possible to gain a good sense of how the system is used in practice, so I would personally endorse the approach. After all, it’s possible to skip on to chapter 3 and follow a sequential approach if this proves to be too forbidding.

Third, in contrast to some introductions, the book promises a pragmatic approach to proof construction or engineering. This is welcome, since Chlipala acknowledges that Coq is a large system that has grown in complexity over the last 20 years. Does he deliver on his promise? The book is divided into four main sections: Sections 1 and 2, “Basic Programming and Proving” and “Programming with Dependent Types,” cover the fundamental technical material. But it is in Sections 3 and 4, “Proof Engineering” and “The Big Picture,” that the author is able to cover the pragmatics of proof. He covers not only common approaches, like logic programming in proof search, but also the problems of larger-scale proof, such as the evolvability and robustness of proofs. This is forcefully communicated through a set of “anti-patterns,” which mitigate against well-structured and evolvable proofs, and provide strategies for avoiding these.

The book itself doesn’t contain exercises, but these can be found on the book’s website. The website also provides access to the full text of the book, the Coq code for all of the chapters, and supporting libraries of code and tactics. It is very clearly written, and the author has a direct, approachable style. If you want to find out more about using the Coq system for building realistic, large-scale proofs, particularly for certifying programs, then I highly recommend this book.

More reviews about this item: Goodreads