3 ms·
In Dijkstra's world, there is no 'real software' but what has been mathematically proven correct. Horribly unworkable in practice, but man, having core librarie
by lmkg 13y ago
In Dijkstra's world, there is no 'real software' but what has been mathematically proven correct. Horribly unworkable in practice, but man, having core libraries & frameworks be formally verified sounds like utopia.
- thibauts 13y agoMathematically proving correct is possible if you have a formal mathematical definition to prove against. So what you're doing is translating the problem from one language to another. This is not the same at all as programming to solve user's problems where the only formal definition is the program itself. The most we can do in this respect is proving the correctness of small parts of ours programs with tests, i guess.