Little Prover
An introduction to writing proofs about computer programs, written in an accessible question-and-answer style, complete with step-by-step examples and a simple proof assistant. 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.
Stats for nerds
9recommend
20mentions
18people
2015–2026years
45% recommend55% neutral
Mentions per year
What Hacker News says
- > to introduce early stage students to Scheme before Python, or deep learning before calculus.
This book is part of the classic "Little" series of books starting with the "Little Schemer" which, despite its name and style, is certainly not a novice beginner book.
The later books: "Seasoned Schemer", "Reasoned Schemer", "The Little Typer" and "The Little Prover" are all very advanced books. They share the same style of illustrations and Socratic method, but you will absolutely need to work through them slowly and careful to get value out of them.
The "Little" books are generally targeted to an audience of computer language nerds and pretty much assume you have a solid understanding of programming, familiarity with scheme and the books come from a time when every serious engineer had basic calc knowledge.
These are classics (and I was really impressed with "The Little Learner") but are very serious and challenging texts, that outside the first book, are aimed at advanced readers (and for those readers are true delights).
- Totally agree. Loved this book. Reading "The Little Prover" right now. I can't get enough of this style of textbook writing.
- Came here to say the same thing. The other books in the series are pretty good too.
E.g. The Little Prover https://mitpress.mit.edu/9780262527958/the-little-prover/
and
The Little Typer https://mitpress.mit.edu/9780262536431/the-little-typer/
- You could study core.logic: https://github.com/clojure/core.logic/tree/master/src/main/c...
I swear I'd bookmarked a resource that was more analogous to #2, but you may want to have a look at The Little Prover: https://mitpress.mit.edu/books/little-prover
- It's going to be hard to learn one way or another. Chlipala's Certified Programmimg with Dependent Types is free online. Then, Software Foundations others mentioned. Starting with lightweight stuff like Alloy or TLA+ might help. Also, The Little Prover book teaches how provers work by letting reader build a small one. Had some decent reviews.
- It looks very nice. The Little Prover, recently published is also a neat small intro.
I wonder how does Software Foundations compare against other more specialized classics in the field like [1-3].
[1] https://mitpress.mit.edu/books/principles-model-checking
Related
The Little Typer
16 recommend · 37
The Little Schemer
288 recommend · 652
Little Learner
10 recommend · 17
2015–2024
Discrete mathematics and functional programming
3 recommend · 4
The little MLer
6 recommend · 15
The little LISPer
28 recommend · 47
2014–2023
Thinking Functionally with Haskell
recommend · 8
