Scan barcode
A review by sritchie
The Little Prover by Carl Eastlund, Daniel P. Friedman
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.