Scan barcode
sritchie's review against another edition
5.0
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/1440327109). 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.
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/1440327109). 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.
blaisepascal's review against another edition
4.0
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.
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.
More...