Neil’s Reviews > Software Foundations, Volume 1: Logical Foundations > Status Update

Working on proofs with Coq is so much fun that it's totally destroying my will to go back and do pencil-and-paper proofs on the Lawvere & Schanuel book … but aside from that inconvenience, this is a wonderful hands-on education in proof technique and types.