Your side point about seL4 is a very interesting portal to the object-capability world. We have long sought a formal definition of plan interference, and that has itself rested upon what makes a plan distinct from an algorithm.
Hyperproperties provide a nice way out of this problem. We can trivially (and perhaps incorrectly) suggest that an algorithm is distinct from a plan in that a plan is the actual source code of a program while an algorithm is the sequence of instructions executed by a machine running the program. We then immediately see that plan interference is a hyperproperty, since perhaps not every run of two interleaved plans will lead to interference.
Oooh nice post!
Your mention of hyperproperties immediately made my mind jump to limplock situations: https://danluu.com/limplock/; I read later on and saw you mentioned partial degradation, which limplock / slowlock would bin underneath. I’m not sure whether large companies use formal reasoning to evaluate their deployments; I’m guessing it would be far far too slow to be practical.
I’m also interested in whether hyperproperty usage can be generalized for any solution to a “gradient problem”, where a non-perfect solution is perfectly acceptable (e.g. spam filtering, ML/AI, content moderation), and whether it just hasn’t because only security research pays off.