[dbaupp]

I'm still not understanding: other than the hardware/global state thing in another comment in this thread[1], what's a program that demonstrates this "composing safe interfaces is unsafe" property? The example in the paper is not one, it was a bug for crossbeam to mark its API safe.

[1]: I'm ignoring this case, because it's somewhat completely impossible to solve: there's no way Rust (or any language) can control this situation. And, there's a strong argument in my mind that this sort of scenario should have an `unsafe` constructor or something, to act as an assertion from the programmer that they're guaranteeing unique access to the resource.

[AstralStorm]

There is a way. You have to meticulously prove operations down to machine code to not have externally observable side effects.

You can weaken the condition by excluding, say, timing effects or cacheline effects. (Say hello to Spectre)

This means you get to prove bounded access and data race freedom on any piece of memory safe code touches. Likewise prove bounded access for all unsafe code and correct cpu flag and state handling.

It it's not as bad as it seems - you can use the machine code prover designed for seL4 as a good starting point.