Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Fundamental proof methods in computer science : a computer-based approach
Arkoudas K., Musser D., MIT Press, Cambridge, MA, 2017. Type: Book (9780262035538)
Date Reviewed: Sep 21 2017

An introduction to proof methods in computer science (CS), this book is set apart from other by its reliance on an interactive theorem prover (called Athena) to achieve the task.

The book begins with an introduction to Athena, which is followed by a section on proof methods that includes chapters on equational reasoning, sentential logic, and first-order logic. Then, more substantial content is introduced in the later sections, in which the authors use natural numbers, integers, and discrete structures such as groups to discuss fundamental data types. There are then sections on proofs about algorithms, and programming languages. Every section contains a detailed exposition of each feature of the language and several pertinent exercises. Most of the exercises are of high quality and are well thought out. Working out these exercises serves as an excellent lesson in writing formal proofs and can be a great source of fun for those who enjoy such exercises. A special mention ought to made of the exercise on the halting problem, which is featured in Section 5.

Some of the choices with regard to exposition are questionable. The authors introduce the formal syntax, illustrated by some basic examples, in the first chapter. This runs into the danger of bogging down the beginner with too many formal details. The official online tutorials of Isabelle and Lean serve as good examples of the gradual exposition of syntax, while simultaneously involving theorem-proving skills.

There is no discussion of the more technical aspects of the underlying logic: first-order logic with many sorts. Such an introduction would have benefited readers more familiar with logic. Another feature of the book that the authors might want to reconsider for a future edition is its length. At over 900 pages, it is a fairly long read even if one creates a course outline using very specific chapters.

The choice of first-order logic with sorts and choices of implementation have led to several elegant features. Some of these features are as follows: equational and implicational chaining are a great introduction to rigorous proofs, and could serve as an introductory lesson in term rewriting systems. The ability to generate proof methods, that is, generalize from specific proofs to tactics for a class of proofs, is a great feature--especially to inculcate ways of thinking about proof methods and not just to solve a particular proof. Features such as module extensions, maketheory, and inheritance of theorems across axiom systems, introduced in the chapters on natural numbers and groups, are useful commands. The authors could have used them to explore further model-theoretic ways of looking at structure.

The downside is that first-order logic with sorts does not have the direct expressiveness of higher-order logic or dependent type theory, which are conventionally used in theorem provers. Thus, Athena is a far cry from what mathematicians informally use in proofs. That makes it difficult to create or prove theorems about more complicated structures. The lack of a direct induction method on variables, despite the means to get around it, is also a bit inconvenient.

Regular courses in logic and discrete structures do not enable a large section of CS students to formulate rigorous proofs. Exposure to theorem proving in proof assistants is seen by the authors as a remedy. Such methods not only introduce students to rigorous proofs, but also provide a familiarity with tools useful in formal verification and computer-aided mathematics. The authors do justice to both of these aspects in the book.

One key area of concern with such an approach, especially when not adequately supplemented with regular math courses, is the formulation of ideas in mathematical language in a rigorous (and meaningful) way. For instance, a nonplanar graph is difficult to formulate rigorously in this proof assistant. With permissible levels of informality, it is possible to state such a property in everyday mathematics.

Questions such as “prove or disprove X” or “construct a counterexample to X” are an indispensable aspect of most math courses. There are very few exercises or examples along these lines. Though there is an Athena feature to check assertions using a finite model counterexample generator, counterexamples can be infinite and the process of reasoning about generating such counterexamples can be rewarding in itself.

Overall, the book is lucid despite the length. It has some really nice exercises and the language has well-thought-out features. The book would make an excellent read as a guide for an elective course or an interesting summer project.

Reviewer:  T. V. H. Prathamesh Review #: CR145558 (1711-0704)
Bookmark and Share
 
Mechanical Verification (F.3.1 ... )
 
 
Computer-Assisted Instruction (CAI) (K.3.1 ... )
 
 
Mechanical Theorem Proving (F.4.1 ... )
 
Would you recommend this review?
yes
no
Other reviews under "Mechanical Verification": Date
Fast automatic liveness analysis of hierarchical parallel systems
Rohrich J.  Programming Languages and System Design (, Dresden, East Germany,271983. Type: Proceedings
Feb 1 1985
Mechanical proofs about computer programs
Good D.  Mathematical logic and programming languages (, London, UK,751985. Type: Proceedings
Feb 1 1986
The characterization problem for Hoare logics
Clarke E.  Mathematical logic and programming languages (, London, UK,1061985. Type: Proceedings
Jun 1 1986
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy