Comment by sirwhinesalot
3 days ago
Too defeatist. If much of the software infrastructure of the world was built on say... Idris, we could do it. That's the promise of dependent types, proof carrying code.
Can we extend that to large scale software? There's no obvious barrier to it, beyond a lack of existing provably correct code to build upon.
I don't expect this to change, however, since the cost/benefit ratio just isn't there. And that makes me sad. We build everything on quicksand.
> There's no obvious barrier to it
It's like saying that there's no barrier to turning lead into gold except for the fact that it's easier to get gold by other means; that's a good thing! The cost of deriving formal deductive proofs is high, while unsound methods are much cheaper and highly effective.
The reason proofs can be expensive is that proving things has an intrinsic computational complexity cost (it's a search problem in a large space). A decade ago I summarised some relevant results of the last three or four decades about the difficulty in proving programs correct: https://pron.github.io/posts/correctness-and-complexity
If software were generally simple enough for all of its interesting properties to be easily proven, that would mean that there wouldn't be much point in the software at all. I think it was a formal methods researcher/practitioner at NASA who once said something like, "computers were built to surprise us; if they didn't, there would be no point in building them in the first place."
> We build everything on quicksand.
You do realise that while an abstract algorithm or a program on the page can be proven correct, it is impossible to prove that a software system is correct, because it's a physical system, and not a mathematical object anymore (you cannot prove that hardware will behave as specified). If mathematical proofs were the only thing that's not "quicksand", then everything in the physical world is quicksand.