What has evolved from the famous century-old (Bertrand) Russell paradox and Russell’s consequent theory of types needs, in my opinion, all the useful elaboration, clarification, explication, and explanation that it can get. Any nontrivial experience in the creation and application of high-assurance, safety-critical (or other) software will eventually engage you in the use of formal methods, where modern type theory now has an increasingly dominant profile.
The book’s intended audience is advanced undergraduates and graduates in mathematics and computing, as well as “mathematicians, computing professionals, engineers, and scientists who need a practical logic for expressing and reasoning about mathematical ideas.” My reading of this excellent and demanding (in the positive sense) book confirms that modern and applicable type theory has come into its own, one could say with a vengeance.
The author states, regarding applicability, “the overarching objective of this book is to transform how logic is taught in university to students who will actually need to use logic in a practical way.” In that regard, he also states that “the practical expressivity of first-order logic is very low compared to that of simple type theory,” although their theoretical expressivities are “comparable.”
First of all, is this a mathematics book or a computing science book? Answer: Yes. The preface states that the Alonzo simple type theory that the book so names and presents “is exceptionally well suited for expressing and reasoning about mathematical ideas.” Its style--and this is not a criticism--is preponderantly that of mathematics: highly subscript-intensive, detailed, and frequently elaborate sequences of definitions, theorems, proofs (or references thereto), and exercises, some of the latter which are in other books. However, and in the author’s words, simple type theory’s “influence on computing has been profound, particularly in the areas of functional programming, formal methods, theorem proving, and constructive logic.” But the trend toward the “mechanization of mathematics” itself has been accelerating over recent decades, with the (arguably unexpected) support of “pure” mathematicians, including Fields Medalists [1,2,3].
I proffer (with apologies for the personal) the following, conceivably human-interest, vignette in support of the author’s above-stated “overarching objective.” At the time of the US’s Sputnik panic, IBM sponsored a special, extracurricular course on finite mathematics for high school students, which used the original edition of the famous Kemeny, Snell, and Thompson book [4]. (John G. Kemeny, of the Manhattan Project and later president of Dartmouth College where he co-created and promulgated BASIC, was a recipient of Einstein’s famous “God does not play dice” remark.) I was surprised, 65 years later(!), to find that Kemeny’s 1949 PhD was sponsored by Alonzo Church and is titled “Type-Theory vs. Set-Theory.” Thus, seeds of the author’s “use of logic in a practical way” were already planted at this early time. The book under review covers (what I construe as) just about everything, including Gödel’s theorems, via the simple Alonzo type theory and its in-book variants.
More than three things stand out about the well-written content of this seminal book, but my three favorites are: its treatment of undefined expressions; the concept and construction of theory graphs (using “little theories”); and the rationale for not crossing “the bridge too far,” dependent type theory [5,6].
As you know, an undefined expression, such as 3.14 divided by zero, makes division a partial function over the reals R; it is a total function over R-{0}. Alonzo’s traditional approach to undefinedness “enables statements about undefined expressions produced by partial functions and definite descriptions to be expressed very concisely.” This serves to streamline, in a correctness-preserving way, an issue that refuses to go away [7,8].
Formalizations of theories are encountered often today, as in a variety of satisfiability modulo theories (SMT) provers. Alonzo supports theory formalization, and further allows a remarkable way of organizing “large bodies of mathematical knowledge”--this by means of (theory-)morphisms as the arcs of theory graphs. “This new style of proof combines the strengths of traditional proofs with the strengths of formal proofs.”
As regards dependent type theory [5,6], which underlies, for example, the now popular Coq interactive theorem prover, the author recognizes simple type theory also as a “stepping stone” to dependent type theory, the “major distraction” in learning the latter being the Curry-Howard isomorphism (its original basis).
I read this book linearly, that is, from first to last page, as a reviewer should. As is the case with many of you, interest in rigorous mathematics (and an understanding of rigor’s incontrovertible necessity in our “serious computing” context) must be constant. A possible “leg up” in determining whether or not this book has a place in your life--it certainly does in mine, and has my highest recommendation--is first to peruse chapter 8, “Proof Systems,” and chapter 15, “Software Support.” These chapters have the additional motivational value of specifically pointing to Alonzo’s real-world practicability, which the many definition-theorem-proof-exercises chapters, though necessary, do not in themselves indicate.
