3 ms·
While it is true that formal methods, despite being able to prevent Spectre/Meltdown, didn't because someone had to think of the issue before proving it doesn't
by pron 6y ago
While it is true that formal methods, despite being able to prevent Spectre/Meltdown, didn't because someone had to think of the issue before proving it doesn't happen, the goal of formal methods is not to prevent all bad things. It is to prevent some bad things. Would you say that you're skeptical of tests because they haven't prevented many bugs, including Spectre/Meltdown, and therefore we shouldn't test?
The only relevant question is, are formal methods effective -- cost/benefit-wise -- in finding problems. Now there's a wide range of formal methods to the point that speaking about all of them as a single category is often not helpful, but the answer to this question is absolutely yes, in the sense that many formal methods have been found to be a very effective quality-assurance measure in many circumstances.