As I was reading, I kept thinking, he should really look at The Little Typer and Pie. Then that was Section V! (Really, many of the books in that series do thi

As I was reading, I kept thinking, he should really look at The Little Typer and Pie. Then that was Section V! (Really, many of the books in that series do this. The Reasoned Schemer for logic programming, The Little Prover for ACL2-style first-order logic.)