Benjamin Pierce has a famous quote: "Attempting to prove any nontrivial theorem about your program will expose lots of bugs: The particular choice of theorem ma

Benjamin Pierce has a famous quote: "Attempting to prove any nontrivial theorem about your program will expose lots of bugs: The particular choice of theorem makes little difference!" (This is also true of mathematical proofs - any attempt to formalize a nontrivial proof will usually expose several minor but fixable bugs in the proof.)