> Correct specification is as hard as correct programming
A complete specification, sure, but that's not really the goal. The things we want to prove are generally just a few key properties: this function always terminates, that one always returns a sorted array, etc. And once you can do that you can impose these things as preconditions: e.g. you must demonstrate that an array has been pre-sorted before you pass it to this function.
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.
A complete specification, sure, but that's not really the goal. The things we want to prove are generally just a few key properties: this function always terminates, that one always returns a sorted array, etc. And once you can do that you can impose these things as preconditions: e.g. you must demonstrate that an array has been pre-sorted before you pass it to this function.