Yes. I am not against all formal methods. Pre and post conditions for loops etcetera. When they are useful they should be used (in many cases they are built

Yes. I am not against all formal methods. Pre and post conditions for loops etcetera. When they are useful they should be used (in many cases they are built in: `for i = k; i < l; i++` has a precondition, a loop condition, and an action all in one statement.) It is the idea, that was very hot thirty or so years ago, that by using formal specifications and rules of inference we could eliminate bugs.