Anyone interested in implementing L4 in rust?


I just read about this OS kernel:

It seems to be an excellent kernel for operating systems such as UNIX, and I hope someone could work out a rust implementation of it.


Maybe check with Sebastian Humenda from TU-Dresden, he did a speech about userland Rust on top of L4 at Fosdem18. He might know more about Rust in L4 kernel space.



SEL4 already has a proof of correctness that is stronger than the guarantees given by Rust’s type system.

It might be that a reimplementation of SEL4 in Rust could be closer to the Haskell version, and hence easier to do than the C one was, but that C version is a sunk cost. It might improve future velocity, but Rust in userspace on SEL4 seems a better approach.