2 ms·
I am impatient with formal verification of programmes. Proving that a programme correctly implements a specification is interesting theoretically but of little
by worik 2y ago
I am impatient with formal verification of programmes.
Proving that a programme correctly implements a specification is interesting theoretically but of little practical use
Correct specification is as hard as correct programming, so the difficult problems are not solved, they are moved.
There are practical use cases for formal methods, but they are rare to encounter
- nyssos 2y ago> 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.
- worik 2y agoYes. 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.