> I agree [...] actually proving it correct is not something that the compiler does Yes. Unsafe blocks are bare assertions, no more. Everything you described a

> I agree [...] actually proving it correct is not something that the compiler does Yes. Unsafe blocks are bare assertions, no more. Everything you described about what happens in Rustc when you use it is better described as making a bare assertion to the compiler. Everything beyond that is socially constructed. Saying it's a proof sounds even more silly when you recall that Rust programmers treat it as quite the opposite -- radioactive markers of places where the program might cause UB. You were trying to characterise it as a proof because you're claiming that "Can Rust prove Linux RCU APIs correct?" is an interesting question. But you are actually asking "Will Rust compile RCU code if we assert to it that using the RCU API is safe?", and the answer is unconditionally yes. It is not an interesting question at all. Your misuse of the word proof led you there, so I am suggesting you stop calling the unsafe keyword a proof. In the broader scheme of things, yes, the way in which Rust encourages you to isolate unsafety is helpful, and so if you wanted something formally verified Rust is a good language for that. That doesn't really translate to RCU, because the hypothetical Rust API would not be an implementation of RCU. All the Iris proofs that have come out of the RustBelt project are bad examples here, because they were actual implementations of things, not APIs around black box implementations that change under your feet when you set kconfigs. As a final thought, here is a supposedly safe-encapsulated Rust API for RCU, I would invite anyone to suggest how writing down this very simple API or similar + a few calls to extern "C" wrappers for the RCU macros could possibly help "prove Linux RCU APIs correct", whatever that means: https://docs.rs/rcu-clean/0.1.6/rcu_clean/struct.ArcRcu.html https://docs.rs/rcu-clean/0.1.6/rcu_clean/struct.ArcRcu.html (Little edit: if you're interested in what circumstances will lead Rust wrappers of C code to elucidate safety, look into rlua, a project to create a safe wrapper for Lua (https://github.com/amethyst/rlua https://github.com/amethyst/rlua). Arguably the main outcome is that we now know that the Lua API cannot be wrapped safely with zero cost, in no small part due to the use of longjmp. Some of RCU's APIs require you do not sleep or block in any way while using it, lest you wake up with the GC train having left the station. For this reason I imagine you won't be able to encode all the usage requirements in the Rust type system, let alone make an actual safe zero-cost API, let alone turn that into a proof of anything.)