Yeah. That's why my preferred approach isn't to use Rust for the core TCB. It'd be mostly unsafe anyway, so what's the point? You can write in an all-unsafe language if you want. you can still prove it correct out of band, and seL4 has done that work for you.
Sure, you could just use unsafe Rust and prove it correct with Prusti or something, but why duplicate work?
alt Hacker News
Yeah. That's why my preferred approach isn't to use Rust for the core TCB. It'd be mostly unsafe anyway, so what's the point? You can write in an all-unsafe language if you want. you can still prove it correct out of band, and seL4 has done that work for you.
Sure, you could just use unsafe Rust and prove it correct with Prusti or something, but why duplicate work?