Boardwalks Across the Tar PitNotes on Chapter 2 of Professor MacKenzie’s Mechanizing Proof: why anyone wanted to prove programs correct.