It seems clear that theories of software should continue to develop this level of formalism if we ever hope to trust it with our lives (eg software-piloted auto

It seems clear that theories of software should continue to develop this level of formalism if we ever hope to trust it with our lives (eg software-piloted automobiles, safety mechanisms, nuclear technology, etc). Imagine if car manufacturers had formal proofs of their claims regarding self-driving car software and it’s predictability / reliability. This is not a situation for trial-by-error.