3 ms·
Program verification is a fool's errand and Dijkstra would have been the first to tell you this. The correct approach is program construction following derivati
by User23 6y ago
Program verification is a fool's errand and Dijkstra would have been the first to tell you this. The correct approach is program construction following derivation rules that do not admit error. You don't need to verify a program produced from a specification this way anymore than you need to prove a proof by construction. It baffles me that to this day the distinction defies comprehension for so many in our field.
- elcomet 6y agoCould you give examples of this?
- User23 6y agoSee this[1] paper. Bugs can still occur of course, but if one restricts oneself to valid manipulations the bugs will be found in the specification and reflected in the code. It's not a magic bullet, and that's one of the reasons TLA+ was invented, it helps with complexity on the specification side. However a method like the one Dijkstra shows in the referenced paper can be used to faithfully implement the TLA+ checked specification. [1] https://www.cs.cmu.edu/~crary/819-f09/Dijkstra75.pdf https://www.cs.cmu.edu/~crary/819-f09/Dijkstra75.pdf
- mycall 6y agoProgram verification is how we got seL4. It isn't a fool's errand.