More precise understanding of faults and how to deal with them can go a long way before suggesting formal verification. Bug is not a fault, but it may cause faults though. You can try to find this bug beforehand or you can deal with the faults at runtime. In practice not just bugs cause faults, but also hardware failures, natural disasters, human mistakes and so on, so you kind of have to deal with faults either way.
> But we can certainly arrange to radically limit the scope of damage available to any particular piece of crap, which should vastly reduce systemic crappiness.
Now, this is the big idea behind supervision trees. Where you split everything into the smallest possible isolated processes and supervisors that watch over them, so that in the event of any process failing it can just get restarted, limiting the scope of the problem to only that one tiny process for the shortest possible time. This idea might even reduce the cost of software development compared to some more popular software development practices. But it does require an easy to use actor model in the language.
> But we can certainly arrange to radically limit the scope of damage available to any particular piece of crap, which should vastly reduce systemic crappiness.
Now, this is the big idea behind supervision trees. Where you split everything into the smallest possible isolated processes and supervisors that watch over them, so that in the event of any process failing it can just get restarted, limiting the scope of the problem to only that one tiny process for the shortest possible time. This idea might even reduce the cost of software development compared to some more popular software development practices. But it does require an easy to use actor model in the language.