Hacker News Reader

Comment by cvwright | Hacker News Reader

Wouldn't that be cool?

Another neat idea would be to build on an existing microkernel like seL4, but write the userspace -- all the drivers, memory manager, filesystems, etc -- in Rust. The NICTA team already has proofs of correctness for the microkernel itself, so why reinvent the wheel? But at the same time, those proofs were super expensive and difficult to make. It would be awesome if we could get a reliable userland more easily by using a better language.

I wonder what it would take to get Rust compiling for seL4?

View on HN

You can already use Rust on seL4, today! It's not ready for public consumption yet since there are no docs, but I've been working on it a lot recently and hope to have a release of the foundational libraries sometime in the next two weeks.

There's a mailing list, if you want to watch: https://lists.robigalia.org/listinfo/robigalia-dev

And the (still in-progress) source code: http://gitlab.com/robigalia/sel4-sys.

I have some ideas about encoding RPC protocols as DFAs in Rust's type system, and then doing verification of the protocols in a more abstract setting (perhaps NuSMV or a similar checker). This is somewhat similar to the (ancient at this point) "protocol compiler" that used to be in Rust, doing a similar thing for channels.

I'm interning at Data61 (née NICTA) on the verification team starting Jan 18, and I'm hoping to transfer some of that experience and knowledge into verifying Rust.

I would love to see some blog posts regarding your experience during this internship.

I am working on some formal verification myself for some commercial projects, and I enjoy reading about stuff like this.

Excellent! Thank you for your work on this. I'll be very excited to see where it goes.

Dream come true!

I've helped work some on a project doing that right now, although it's mostly been the awesome cmr.

https://gitlab.com/robigalia/sel4-sys

Not much, really. The main thing needed is to port the language runtime to seL4. This should be a relatively small effort, and a great project to both learn some of the underbelly of Rust's ABI and seL4.

Already done :)

I saw a sibling reply posted shortly before mine outlining your work. Nice job. :-)

> why reinvent the wheel

Why not.

It's /only/ 30 man years of effort from experienced engineers. http://ssrg.nicta.com.au/publications/nictaabstracts/Klein_A... page 56.

Reply on news.ycombinator.com