Earlier quoted context omitted.
There are realistic systems that are operationally secure by the given standard. Nuclear launch systems are the obvious example. “Best practice” is a euphemism for whatever it is the majority does. Nobody ever got fired for buying IBM. That’s not even reasoning. Finally, your paragraph about sandboxing is ill considered, but not that wrong. First all programs have operational semantics, the only question is how well…
> There are realistic systems that are operationally secure by the given standard. Nuclear launch systems are the obvious example. AFAIK there aren't really any examples of production systems that have meaningful, formally verified security properties without gaping holes. Do you have a good paper about the full stack formalization/verification of a nuclear launch system? > “Best practice” is a euphemism for whatever…
Bwahahaha you're funny.
> If you try to formalize everything, you'll drown. If you strategically concede defeat and admit that some parts of the system aren't possible to formalize, you can get a lot of strong guarantees.
You're contradicting yourself again. There's a reason why weakness is a strength in formalisms.