Comment by tkz1312

> This enforcement wouldn't even be possible in C or any other language I know of personally that'd be efficient to write an OS in.

The sky is the limit when it comes to verification of complex properties for C programs. You “just” need a few expert level theorem prover users and a couple of years :)

If you’re actually operating in the kind of domain where exhaustive verification is worth the time investment, C blows Rust out of the water (due to it’s simple semantics and mature ecosystem of verification tooling). There remain no formal semantics of the surface level rust language (and constructing one is a daunting task given its deep and baroque complexity). Verification at the MIR or LLVM levels may be more tractable, but I’m not aware of any large scale results here. C or assembly in combination with some verification tooling remains the gold standard for fast and correct software at the highest level.

Rust offers reasonable memory safety in a relatively accessible and fully automated package. It’s a better choice than C for the majority of cases, but it’s far from the last word when it comes to safety.

btw (and as noted in a sibling comment), sel4 is fully verified down to the assembly level.