Little Prover
by Daniel P. Friedman, Carl Eastlund, Duane Bibby · first published 2015
50% recommend50% neutral
Why HN recommends it
Gentle, dialogue-style introduction that teaches how theorem provers work by having the reader build a small one; suits readers who enjoyed The Little Schemer and want an intuitive path into logic and formal proof.
Summarised by Claude from recommending comments
Affiliate links. As an Amazon Associate I earn from qualifying purchases.
Mentions per year
What Hacker News says
Related books
2018–2026The Little Typer
Daniel P. Friedman, David Thrane Christiansen
Recommended by 16 · mentioned by 3316 recommend · 33 mention16 recommend · 3316 recommend
2023–2026Little Learner
Daniel P. Friedman, Anurag Mendhekar
Recommended by 10 · mentioned by 1510 recommend · 15 mention10 recommend · 1510 recommend
2007–2026The reasoned schemer
Daniel P. Friedman
Recommended by 45 · mentioned by 7945 recommend · 79 mention45 recommend · 7945 recommend
2007–2026The seasoned schemer
Daniel P. Friedman
Recommended by 33 · mentioned by 4733 recommend · 47 mention33 recommend · 4733 recommend
2008–2025The little MLer
Matthias Felleisen
Recommended by 6 · mentioned by 116 recommend · 11 mention6 recommend · 116 recommend
2011–2022Certified Programming with Dependent Types
Adam Chlipala
Recommended by 25 · mentioned by 3125 recommend · 31 mention25 recommend · 3125 recommend
2007–2026The Little Schemer
Daniel P. Friedman, Matthias Felleisen
Recommended by 288 · mentioned by 438288 recommend · 438 mention288 recommend · 438288 recommend
2008–2025The little LISPer
Daniel P. Friedman
Recommended by 28 · mentioned by 4328 recommend · 43 mention28 recommend · 4328 recommend
…Stephenson, and H is for Hawk by Helen Macdonald. The former is likely known to the HN crowd; the latter draws comparisons to T.H. White's classic The Goshawk. Among non-fiction books, I enjoyed The Little Prover by Friedman and Eastlund. It was exactly what I expected, a gentle introduction into inductive proofs in the idiom established by The Little Schemer.
on “Ask HN: Best books you've read in 2015” ↗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…
on “Software Foundations by Benjamin Pierce et al.” ↗…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.
on “A formalization of category theory in Coq” ↗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
on “The birth of Prolog (1992) [pdf]” ↗Glad too see that I am not the only person to quite excited about the The Little Prover. Don't think I have ever felt this way about the release of a CS book.
on “My Top 100 Programming, Computer and Science Books: Part Four” ↗Not the author but a recent book I've read on the subject served as a gentle introduction for me: The Little Prover [0]. If you can get past the lisp syntax you can get through this book with an informal and incomplete education in set theory and an intuitive understanding of logic. [0] https://mitpress.mit.edu/index.php?q=books/little-prover
on “The C standard formalized in Coq” ↗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/
on “Ask HN: Which books have made you a better thinker and problem solver?” ↗Totally agree. Loved this book. Reading "The Little Prover" right now. I can't get enough of this style of textbook writing.
on “Ask HN: What's the "best" book you've ever read?” ↗…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"…
on “The Little Learner: A Straight Line to Deep Learning” ↗https://mitpress.mit.edu/books/little-prover The Little Prover Written by Daniel P. Friedman and Carl Eastlund https://the-little-prover.github.io J-Bob J-Bob is our little proof assistant, available on Github. For an introduction to J-Bob,…
on “ACL2” ↗…(look up Prolog and Datalog as languages in the same vein). The Little Typer is the linked book covering type systems and, specifically, dependent typing. The Little Learner covers machine learning. The Little Prover uses the same format and has you develop proofs. Little, Seasoned, and Reasoned are, IMO, the better books in the series to start with. I found the later ones to be good but very dense and not always…
on “The Little Typer (2018)” ↗…bounded search and can't be applied directly to implementations. I personally don't confer that much trustworthyness to systems that appeal to model checking tools for their correctness. I've seen The Little Prover, but am somewhat wary of it. On the other hand, I enjoyed The Little Schemer very much. I might take a look at it next month.
on “Software Foundations by Benjamin Pierce et al.” ↗My current reading list: - Fundamental Proof Methods in Computer Science - Handbook of Practical Logic and Automated Reasoning - Software Abstractions - The Little Prover Yes, currently I have Athena, OCaml, Alloy, ACL2 (via Dr Racket/Dracula) all up and running to work through the exercises in these books. I'm very skeptical anything will come of this, but it interests…
on “Coming Soon: Machine-Checked Proofs in Everyday Development” ↗I'm about to start reading "The Little Prover" (https://mitpress.mit.edu/books/little-prover) which sounds like a good intro.
on “Dramatically Reducing Software Vulnerabilities [pdf]” ↗Whatever your views on that stuff... it is fun to play in Coq. On the other hand, playing with J-Bob, the toy "proof assistant" used in The Little Prover is tedious at best. I'm torn between just giving up with the last two chapters of the book undone.
on “Software Foundations by Benjamin Pierce et al.” ↗