3 ms·
Proving safety is just a small part of the problem to be solved. The hard part is actually structuring the program such that its correctness can even be formula
by ulrikrasmussen 2y ago
Proving safety is just a small part of the problem to be solved. The hard part is actually structuring the program such that its correctness can even be formulated as a formal property which can be proved. For a lot of software that alone is highly nontrivial.
- recursivedoubts 2y agoFrom "No Silver Bullet": > More seriously, even perfect program verification can only establish that a program meets its specification. The hardest part of the software task is arriving at a complete and consistent specification, and much of the essence of building a program is in fact the debugging of the specification
- 986aignan 2y agoOn the other hand, proofs sometimes give you more than you'd expect. A proof that the implementation of a function always returns some value automatically proves that there's no arbitrary code execution, for instance.