[SenAnder]

Formally verifying does no good if the compiler is infected. In the stuxnet example, formal verification wouldn't even help - how do you formally verify centrifuge timings?

Unlike what your sibling comment claims, I'm not saying all software is equally important, or must have equal effort invested in securing it. But insecurity absolutely is infectious, and the more insecure the general environment is, the harder it is to secure a small part of it.

For example, you'll want a compiler. How secure is the web stack of the page that delivers your gcc/clang? How secure is its host's infrastructure, and of the DNS provider? The browser you're downloading it with? Did you ever visit any other page that might have compromised it? What about your text editor, your OS, the SDK you're using to flash code onto the pacemaker.. And all of them have vast supply-chain networks.

[trealira]

Hopefully, for the pacemaker, the authors of the code would be using a verified compiler like CompCert (although it's only verified for the compilation, not the parsing or the preprocessor), but you don't have control at every level, like for the hardware. You can't verify centrifuge timings, but you can specify software and verify that it fits the specification to the point that it won't be the point of failure (assuming you have everything under control, like the pacemaker SDK, everything). I do see what you're saying about it being infectious, though.