The Little Prover

by Daniel P. Friedman, Carl Eastlund

The Little Prover introduces inductive proofs as a way to determine facts about computer programs. It is written in an approachable, engaging style of question-and-answer, with the characteristic humor of The Little Schemer (fourth edition, MIT Press). Sometimes the best way to learn something is to sit down and do it; the book takes readers through step-by-step examples showing how to write inductive proofs. The Little Prover assumes only knowledge of recursive programs and lists (as presented in the first three chapters of The Little Schemer) and uses only a few terms beyond what novice programmers already know. The book comes with a simple proof assistant to help readers work through the book and complete solutions to every example.

Genres: Computer Science, Programming, Software, Mathematics, Computers, Nonfiction, Technology

248 pages, Paperback

First published July 10, 2015

About the author

Daniel P. Friedman is Professor of Computer Science in the School of Informatics, Computing, and Engineering at Indiana University and is the author of many books published by the MIT Press, including The Little Schemer and The Seasoned Schemer (with Matthias Felleisen); The Little Prover (with Carl Eastlund); and The Reasoned Schemer (with William E. Byrd, Oleg Kiselyov, and Jason Hemann).

Reviews

[Sam Ritchie · Rating 5 out of 5]

Certainly not as mindbending as the earlier books in the series, like the Reasoned Schemer. This was a great introduction to the idea that you can write programs that can act as proofs for other programs. I'd love to start using this stuff instead of quickcheck. Quickcheck properties are basically theorems about your code. Without lisp and the AST, you're forced to just throw inputs at the definitions. Being able to prove some of the lower level functions in Algebird correct would have been just enormously useful and interesting.

The practice you get here with inductive reasoning should make it easier to digest Coq, Agda and Idris tutorials. Recommended!

Edit, 11/12:

I'm coming back to add to this review after finishing a review of Gödel's Proof (https://www.goodreads.com/review/show...). That beautiful book helped me realize what a "formal system" actually is, and why a system like the little prover can actually mechanically search for "proofs", or paths, to a "theorem", or a valid configuration of Scheme syntax, in the case of this book. Coding is fun enough that you often don't need context. Still, context is hugely helpful when trying to develop some feeling for math, for proof, and for how a proof system like the one described in this book is similar to proofs you'll find out in the wide world. Extra-recommended now that I know more about the field.

[Steve · Rating 5 out of 5]

Don't be intimidated by this book; The flavor of Scheme used is extremely minimalist with only a few simple uses of recursion and the concepts of rewriting and defining theorems are explained with thorough examples. You will have to don your thinking cap to convince yourself that certain rules and theorems are correct but I think you'll find it rewarding, I certainly did.

[Blaise Pascal · Rating 4 out of 5]

The Little Prover is a book on learning how to inductively prove programs correct. Like the other "Little" books by Friedman, it is written in a question/answer style, and uses a dialect of Lisp as the main computer language.

The proof technique used is basically a rewriting schema, where the idea is to "prove" a statement by applying a series of theorems and axioms which allow you to rewrite the statement, ultimately attempting to rewrite it to 't, or true. Rewriting theorems include the ability to rewrite "(if a c c)" to just "c" for any value of "a" and "c" (and the converse: rewrite "c" to "(if a c c)" for any value of "c" and "a", if that's helpful), rewrite "(equal a a)" to 't, rewrite "(if 't x y)" to "x", and so on. There are 21 rewrite rules given. Most of the book introduces these rewrite rules and gives you practice in using them.

Also discussed is a proof assistant called "J-Bob", which implements the Lisp dialect used in the book and provides an interactive tool to help write the proofs. I am not enamored by the syntax of parts of J-Bob, especially the syntax needed to give a "path" to the "focus" of a rewrite rule. For instance, to apply the "equal-same" rewrite rule to the statement "(if (if (atom b) (equal 'polar 'polar) 'f) (equal a 'bear) 't)" you'd have to specify the "path" (Q A 1), meaning the question of the first if, the answer to the second if , and the first argument to the function application, which is "(equal 'polar 'polar)". Each step in a proof uses a path based on the results of the previous step, so it is hard to read a proof in J-Bob and picture exactly how the transformations are going to understand the proof.

Of the 218 pages of the book (not counting frontmatter and backmatter, 162 are the main text, 15 are an introduction to using J-Bob, 20 are all the proofs in the book in J-Bob syntax, and 12 are the implementation of J-Bob itself. While I think the use of an interactive proof helper is useful, devoting almost 50 pages of a rather short book to the proof helper seems a bit much, especially one that is not quite as user-friendly as it could/should be.

Ignoring J-Bob, the book sometimes goes a bit fast. It may ask the question "Can we simplify this focus in this statement? (...)" with the answer "Sure, by using foo, then simplifying with bar, bat twice, and bar again. (...)". While the use of foo is perhaps easy to see (we are in the part of the book teaching about foo...), it isn't until after using foo that we would see how to apply bar, bat, and so on. Those intermediate steps are mentioned, but not shown.

I wish the "Little" books were available in an electronic format, as it would make it a lot easier to work through the book with an editor and/or lisp interpreter at hand without having to hold open the book with one hand and type with the other.

Over all, if you like the style of the other "Little" books, which I do, despite the gripes above which are frankly common to all of them, you'll probably like this one as well, and learn about inductive proving and proof assistants along the way.

[Matt Diephouse · Rating 4 out of 5]

Like the other books in the series, I've found the format of The Little Prover to be a little disappointing at times. I can't help but think that a little straightforward prose would be helpful here-and-there.

But overall, I found the content of this book helpful. I haven't thought much about software proofs, so this was an educational introduction to the topic. The book ends with some interesting references, so I'm hoping that will lead to some more good material.

I also find the use of Scheme to be disappointing. In some ways, the lack of syntax provided by Lisp makes learning easier. But I find that the lack of a type system results in sloppy programming that's harder to read and follow along with.

[Tony Poerio · Rating 4 out of 5]

The Little Prover is effective and fun. Inductive Proofs can sometimes be an incredible pain, but this makes them more approachable, and I appreciate the author's attempt to make the whole concept and process simpler and more intuitive--he does.