We are all familiar with the need to prove the properties of a particular computational process. This is the problem of verification. What is not immediately obvious is that such proofs can be turned on their heads and used as mechanisms for classifying the computations whose properties they prove. This book explores the deep relationship between formal proofs and notions of computation.

Written by two leading practitioners in the area of formal logic, the book provides a panoramic view of the topic. Starting with the basics of propositional logic, the authors lead us through the topics of recursion theory, provable recursion, and higher-order functions. The final chapters are devoted to the extraction of computational content from formal proofs themselves. This technique has the catchy slogan “code carrying proof.”

The presentation follows the specific interests of the authors, as they note in the preface. This personal touch makes the book all the more interesting and useful, as there is a uniformity in the presentation of concepts from beginning to end. This is balanced by copious references to and notes about alternative and competing concepts. The authors also provide proofs for all significant theorems. This makes the book a reference volume as well.

Part 1 covers well-known material on theories of proof and recursion, leading up to a presentation of Gödel’s theorems. Part 2 deals with hierarchies of provably recursive programs and ties together the logical complexity of inductive proofs and the computational complexity of recursive programs. Part 3 develops higher-level computations and a theory of computable functionals (TCF), the proofs of which can be interpreted as programs. Three different proof interpretations are discussed and proved sound.

A good way to read this book is to first skim over the entire volume, building up an idea of the progression of concepts; then, visit and revisit topics of interest and follow the detailed threads of concepts forward and backward through the entire volume. Each chapter is reasonably self-contained and offers some interesting concepts and significant results. Each new reading can furnish insights that were missed in earlier readings, and there is a lot to be learned from the combined insight and experience of the authors.

This reference volume is a must for the bookshelf of every practitioner of formal logic and computer science.