4 ms·
That would be the purpose of formal proofs, wouldn’t it? Formal proofs may not be silver bullets, and we’re never safe from a faulty implementation of the prov
by ElFitz 2y ago
That would be the purpose of formal proofs, wouldn’t it?
Formal proofs may not be silver bullets, and we’re never safe from a faulty implementation of the proven algorithms, but this quanta article on a DARPA project showed impressive results [0].
There’s also AWS’ use of TLA+ [1].
[0]: https://www.quantamagazine.org/formal-verification-creates-hacker-proof-code-20160920 https://www.quantamagazine.org/formal-verification-creates-h...
[1]: https://news.ycombinator.com/item?id=22082869 https://news.ycombinator.com/item?id=22082869
- thaumasiotes 2y ago> Formal proofs may not be silver bullets, and we’re never safe from a faulty implementation of the proven algorithms You also aren't safe from misunderstanding what it is that you've proven about the program. Which is actually the same problem as other software bugs; you have a specification of something, but you don't know what it is that you've specified, and you wish it were something other than what it is.
- Nevermark 2y agoToo true. When we translate complex concepts to code & math, either may inadvertently not be exactly what we wanted. Interesting to think about a formal code verification system that maintained a connection between all four prime artifacts: natural language description of problem as understood & intended solution, vs. code and the properties actually verified.
- spc476 2y ago"Beware of bugs in the above code; I have only proved it correct, not tried it." ---Donald Knuth
- ElFitz 2y agoI will remember that one.
- PeterisP 2y agoFormal proofs can only prove that the system matches a specification. Many (most?) non-trivial bugs are actually flaws in the specification, misunderstandings about what exactly you wanted and what real-world consequences arise from what you specified.