3 ms·
The problem with formal verification is that in practice, many problems can't even be formally specified. Try formally specifying the requirement "the GUI shoul
by adwn 5y ago
The problem with formal verification is that in practice, many problems can't even be formally specified. Try formally specifying the requirement "the GUI should work as expected" – it's hard enough even to test this, and impossible to formally specify.
Of the remaining problems, the complete, formal specification would be larger, more complex, and more bug-ridden than the implementation. "Hey adwn, can you add a button to the GUI so the user can export the current dataset to a CSV file?" Maybe 20-50 lines of code, but a full specification would be a multi-year project – and it would be almost certainly wrong.
- AnimalMuppet 5y ago> The problem with formal verification is that in practice, many problems can't even be formally specified. And even if they can, where does that formal spec come from? Sooner or later, it comes from some informal understanding of what's supposed to happen. Well, how do you check that the formal spec is correct? Because if you can't do that, all formal verification can do is tell you that your program correctly implemented the wrong thing. And I don't think you can do that. First, I don't think you can go from informal to formal by formal means. Second, even if you can, you still can't verify the informal spec. So formal verification can only go so far. I can recall several things that were bugs in the spec. Log4j is the most recent example. Heartbleed I think was a specification bug. Back in the day, a lot of computer viruses were helped on their way by bad ideas in the specification of Microsoft Outlook.