Chilpala's text Certified Programming with Dependent Types 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 colour theorem – and also those in the domain of theoretical computer science. Indeed, the “POPLmark challenge” http://www.seas.upenn.edu/~plclub/poplmark/ has set a benchmark for proof mechanisation 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?
Firstly, Chilpala 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 that 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 result 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 co-exist gives a type system that can express program pre-conditions, 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.
Secondly, Chilpala opens the exposition in Chapter 2 with a worked set of examples that concentrate on language evaluators and compilers. Rather than covering all 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 reading this that anyone reading the chapter needs to understand a language like Haskell or ML, but with that knowledge it is possible to gain a good sense of how the system is used in practice, and so I would personally endorse it. After all, it's possible to skip on to chapter 3 and follow a sequential approach if this proves to be too forbidding.
Thirdly, in contrast to some introductions, the book promises a “pragmatic” approach to proof construction or engineering. This is welcome, since Chilpala acknowledges that Coq is a large system that has grown in complexity over the last twenty years. Does he deliver on his promise? The book is divided into four main sections: the first two cover the fundamental technical material, namely “basic programming and proving” and “programming with dependent types” in some 250 pages, but the remaining two sections (130pp in total) cover “proof engineering” and “the big picture” and it is in these two that he is able to cover the pragmatics of proof. He covers not only common approaches like logic programming in proof search but 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 provides strategies for avoiding these.
The book doesn’t contain exercises, but these can be found on the book website, contributed by readers. The website also provides access to the full text of the book, as well as the Coq code for all the chapters, as well as supporting libraries of code and tactics. It is very clearly written, and tha 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 recommend this highly.
