3 ms·
There is a pervasive, cultural lack of formal verification in software, and it's risky, terrible, and should be stopped. Formal verification can takes multiple
by burnt-resistor 2y ago
There is a pervasive, cultural lack of formal verification in software, and it's risky, terrible, and should be stopped. Formal verification can takes multiple forms and operates at different spans across the layers of the stack. We need more of it to prove the correctness of compilers, libraries, and programs. It is a lot of work, but it's critical to proving things are as good, as say, seL4.
- johnisgood 2y agoWe need more Ada / SPARK!
- tlarkworthy 2y agothere is a culture of type safety which is a very watered down machine checked proof that the thing entering a function has affordances X,Y and Z. Its not the end to end functional verification you are talking about but its not nothing either.