I happened to initially open this very advanced, excellent monograph to chapter 12, “Toward Constructive Logic as a Practical 4GL [fourth-generation language].” The authors certainly speak for many of us who “would like to solve problems by building well-structured, comprehensible, correct programs solely through reasoning with domain knowledge.” The authors point out in chapter 1 that the proofs-as-programs paradigm was proposed 30 years ago as a means of translating domain knowledge directly into correct software, without having to invoke orthogonal programming language expertise.

The collective experience of the software development community over several decades has determined without a doubt that there is, in Euclid’s words reputedly directed to upper management, “no royal road” to achievement of this worthy goal. The authors are indeed very realistic and modest: their book “details several important advances” in “applying constructive techniques to industrial-scale, complex software engineering problems,” by means of their Curry-Howard protocol, to effect generalization of proofs-as-programs (Part 2 of the book) within functional programming; imperative proofs-as-programs (Part 3), or proofs-as-imperative-programs; and structured proofs-as-programs (Part 4).

The preface opens with the following statement: “This book finds new things to do with an old idea. The proofs-as-programs paradigm constitutes a set of approaches to developing programs from proofs in constructive logic.” We are already in advanced territory, here in the preface, at least with respect to a run-of-the-mill user of formal methods such as myself.

Another advanced theoretical underpinning of the book is the Curry-Howard isomorphism or correspondence, in which ordinary intuitionistic logic corresponds to a logical type theory, intuitionistic proofs correspond to terms, formulas correspond to types, and logical rules correspond to type-inference rules. (The book seems to use “intuitionistic” and “constructive” as synonyms.)

The Curry-Howard isomorphism, by now a time-honored result, is a great discovery that was never obvious enough to have leapt out from back-of-the-envelope scribblings; hence, there is no long discussion of the isomorphism itself in the book, though the references thereto are ample. The book’s focus is not the isomorphism/correspondence itself, but is rather on the Curry-Howard protocol (chapter 3) that the authors have created on the isomorphism’s basis. “The protocol specifies a minimal set of properties to be satisfied by a logic and programming language” so as to enable the Curry-Howard isomorphism to be effective in generalizing today’s state-of-the art proofs-as-programs to their imperative and structured counterparts. The authors clarify their Curry-Howard protocol by explicating its ontology. The domain of logic is the (Gentzen-style) natural deduction system, which defines a logical calculus formally. The domain of proofs is a logical type theory (LTT), which, by means of the Curry-Howard isomorphism, allows proof encoding with types as statements, terms as proofs, and type inference as logical inference. The domain of a programming language is a computational programming language type theory (CTT) with operational semantics.

The third leg of the book’s underlying theoretical tripod is, as I construe it, (knowledge of) the lambda calculus, and its realization in such functional programming languages as standard metalanguage (SML), functional and procedural (imperative) constructs of which are used in the book.

I wish to give the potential reader of this original, innovative, and very advanced monograph an idea of its level. At the risk of sounding like the proverbial buzzword-hyena, I’ll enumerate additional terms of art that I encountered in reading the book sequentially: skolemization; many-sorted logics; second-order logic; Konig’s lemma; abstract data types; Church-Rosser property; Hoare logic and triple; signatures; categories, functors, and morphisms; transitive closure; total functions; sequents; partial and total correctness; Heyting integer arithmetic; soundness and completeness; model theory; pushout construction; and Kripke semantics. Some of these have only casual import.

I hasten to add that each chapter is very nicely bracketed with an initial, clear description of strategy and a final, equally clear summary of conclusions. This expository technique provides an indispensable intelligibility to the nonexpert and expert alike, at their respective levels of reading.

The phrase, “Progress waits for no one,” came to mind as I was approaching the last chapter of this excellent, substantive monograph. The book has left me nothing less than astounded by advances in, and the solid promise of, research in proofs-as-programs and in its formal methods superset. It seems that, while I was doing my day-in and day-out defense to upper management of plain vanilla formal methods for the construction of safety-critical software, the theoretical infrastructure for creation of error-free, specification-compliant systems has, thanks to the authors’ and their colleagues’ research, grown deeper, richer, and more solid. The future looks bright.