3 ms·
Formal methods have seen adoption in hardware where the cost of bugs is much higher. The fact is it’s cheaper to patch buggy software than it is to apply formal
by slededit 8y ago
Formal methods have seen adoption in hardware where the cost of bugs is much higher. The fact is it’s cheaper to patch buggy software than it is to apply formal methods. Quality has remained above a level that would impede progress, and basically it just isn’t that big of an issue.
On a smaller scale it’s been used in code checkers to find uses of uninitialized variables and “can be null” errors. Just in a limited form.
- repolfx 8y agoI used to believe that was true, but recently I read that even in the hardware space formal methods have limited application - like software, they're usually used only on very specific sub-parts like MESI protocols. But it's not the case that a modern CPU is extensively applying formal methods. W.R.T. things like static type systems, I agree. But progress there has been fairly minimal in the widely adopted languages. Mostly, in fact, the type systems did not get stronger, but the focus was on making them easier to use through more type inference.
- slededit 8y agoFull top down proofs are rare but it’s more common at the module level.