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.
1 Like
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.
https://crustulus.de/2017/07/rustonl4re-safelanguagemeetssafekernel/
2 Likes
Why?
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.
5 Likes
Seems it is already done within Robigalia project. Here you can find their sources. But the site and repo seem dead, so someone might want to continue the project.
It wasn't clear to me what 'it' referred to in your post. To clarify for others reading: robogalia has a rust API for SEL4, not a reimplementation of L4 in rust.