Hacker News Reader

Sadly, I share your pessimism about formal methods. I suspect one of the headwinds is that there's a greater demand for more software than there is for better-proven software.

View on HN

At the end of the day I think it's just a matter of cost. If it's cheaper to let a software fail and simply fix it when it does, there will not be much interest into proving it to be correct. If a failure will likely be vastly more expensive than proving correctness, then proving correctness will make sense. There are simply way less instances of the second category. I think one of the few "new" instances, which might be worth mentioning is smart contract programming, where failures can cause millions of loss and proving correctness is not too expensive.

With the amount of infrastructure focused around testing I think the opposite is true.

I think it's more ignorance and culture. Many people don't know about formal methods.

Agreed.

Having better-proven software is a precondition to having more software. Especially if you expect that things like program synthesis are going to be increasingly important - who wants to "synthesize" buggy code?

Reply on news.ycombinator.com