Chilpala intends, by means of this book, “to convince you that the technology of program verification is mature enough today that it makes sense to use it in a support role in many kinds of research projects in computer science.” The book, though by no means an easy read, is nevertheless fully convincing in that regard, and is also successful in its further purpose of providing “a handbook on practical engineering of certified programs with the Coq proof assistant.” This rather intricate and code-intensive work will be much easier reading for those who routinely use such functional programming languages as ML, Haskell, or OCaml; comfort with, and a certain mastery of, functional programming is practically a prerequisite.

The book can, in accord with the author’s own characterization, be said to encompass well-annotated Coq code, including intermittent, automatically extracted OCaml code. The style, which is by design anything but linear, is somewhat reminiscent of Knuth’s literate programming [1], where a collection of ideas (expressed in natural language) and code (Coq components and OCaml) at various levels of abstraction is woven as what I might call a pseudo-Knuth-web. (An Internet search will reveal the existence of “coqweb,” which is closer to actual literate Coq programming.)

My current job of managing the safety certification of computer-controlled systems, and previous jobs designing them, virtually forced on me the awareness of (the practicality of) formal methods as the road to provable correctness of designs and programs. Correctness, in these venues, refers to safety of life, limb, and the continually safe and proper functioning of extremely expensive equipment. There is, in that real-world domain, an understandable (if ultimately unreasonable) tension between the budget-and-schedule stakeholders of a project and the project’s design-safety certifiers (whose injection of proof-intensive formal methods into this mix is invariably viewed with great skepticism and suspicion). So also here, in chapter 16 (“Proving in the Large”) of the present esoteric work, there is the observation:

Most researchers and practitioners in software assume that mechanized theorem proving is profoundly impractical. However, starting around the beginning of the 21st century, there was a surge in the use of proof assistants in serious verification efforts.

This book, if read in my view the wrong way, could reinforce, in those already so inclined, the view of Coq’s highly advanced set of formal methods as being profoundly impractical. But I can certainly vouch for the great practicality of judiciously applied formal methods in the design and certification of safety-critical systems, if the apples (B method [2,3]; first-order logic; set theory) to oranges (Coq; Gallina, Coq’s specification language; Ltac, Coq’s domain-specific language for proof-search procedures) comparison can be tolerated. In fact, I consider the oranges really to be another species of apple, or vice versa; the “big idea” here is proofs.

One minor contribution to my interest in this book is a snails-pace background project of re-expressing a homegrown, throw-away C++ based proof-engine as a functional program. I think that, for this and other reasons, Coq transcends the above-mentioned support of “research projects in computer science,” so as to compete with other real-world realizations of proof-based certifications [4].

The second-biggest idea underlying this book (and Coq itself), proofs being the primary idea, is the Curry-Howard correspondence or isomorphism, which “states a formal connection between functional programs and mathematical proofs,” thus allowing use of “the same type-checking technology” for validating both proofs and programs. “In fact, functions and implications are precisely identical according to Curry-Howard!” (author’s emphasis). In this regard, further solid theoretical background can be obtained via the outstanding book-length treatment by Poernomo, Crossley, and Wirsing [5], who define a Curry-Howard protocol for proofs-as-programs that can be applied to functional programs, and also to imperative-language and structured programs.

Coq is founded on constructivist/intuitionist logic; the logic behind Coq’s proof engine is CIC, the calculus of inductive constructions. CIC “differs from set theory in starting from fewer orthogonal primitives.” One of my favorite sections is 4.2, “What Does It Mean to Be Constructive?” (See also Schechter [6].) The author’s answer “comes from the fact that Coq implements constructive or intuitionistic logic ... . In constructive logic, classical tautologies like ... P or not-P do not always hold.” The section on choice axioms makes vivid that these axioms are also controversial in mainstream mathematics. The explications will enrich all who read them, from intuitionists to formalists, however dyed-in-the-wool they may be. They show what I might call intermediate-level consequences of choice axioms, without the necessity of having worked up to the Banach-Tarski paradox of two identical spheres for the price of one.

This substantive book was very much worth my struggle, and should serve to enlighten all who read it. I will follow the author’s concluding advice: “Read through the Coq manual, front to back, at some level of detail.”

More reviews about this item: Goodreads