Interesting, but sounds like much more than a lifetime achievement. As far as I understand, it is written in Rust; this raises the question of whether there are significant differences to Redox OS, which seems to share most of the goals. But sel4 on the other hand is written in C; are you going to migrate sel4 to Rust?
Like I said, it's not meant to be a "Rust OS" and will incorporate a lot of C code still (and various other languages as well). I doubt that the kernel will ever get completely rewritten in Rust, although eventually some Rust code might get added (once I break up the giant kernel lock I am thinking I'll use the same locking library I'm using in the process server, so that would add some Rust code to the kernel). I don't see a lot of point to rewriting the kernel since it's probably not going to see lots of new code being added all the time and is generally pretty limited as to what it includes (I'm not quite as reluctant to add stuff to the kernel as the seL4 developers are, but I still am going to try avoiding it unless there's no other good way to do something).
Redox has several of what I consider to be questionable design/implementation decisions. I explained a couple of them in a previous comment (the limited filesystem namespace and IPC models and the lack of real-time support). Some other things include the weak implementation of locking (it uses pure spinlocks instead of something like the adaptive queue-based locking that I'm using in the process server), a rather limited heap allocator that doesn't support growing/shrinking the heap or custom object sizes for slabs (the heap allocator I'm using is a derivative of the same one that Redox uses but it's been heavily enhanced with support for shrinking/growing the heap and custom slab sizes), and the rather boilerplatey implementation of some of the libraries (for example fork() is implemented as a library function that copies process context through a filesystem-based API, but rather than having object-oriented wrappers on top of the filesystem for the various state objects that it's manipulating, the fork() implementation directly invokes open(), read(), and write() a lot).
That's interesting, thanks for the explanations. Which of the many OS text books do you think covers the topics you are confronted with in this projectk best (especially how to implement an efficient microkernel and integrated ipc)?
