“Attempting to prove any nontrivial theorem about your program will expose lots of bugs: The particular choice makes little difference!”