> there could be bugs in unsafe code in the standard library
For any embedded work or kernels, you wouldn't be pulling in the standard library via a `#![no_std]` attribute.
But you're right that bugs in the compiler could produce safety issues.
For any embedded work or kernels, you wouldn't be pulling in the standard library via a `#![no_std]` attribute.
But you're right that bugs in the compiler could produce safety issues.
Perhaps not, but in a kernel you'd have plenty of your own unsafe code.
SEL4 doesn't.
There are, of course, people thinking about bridging the worlds of formally provable correctness and Rust, e.g. https://github.com/rust-lang/rust/issues/18496 though extraction based is likely to not produce the most elegant or efficient code... and I assume the along-the-side proofs like SEL4 uses would be harder for Rust because the language is more complex than C.