But today, that's not the only way to guarantee isolation. We may also be able to do it via type systems. If we could create things statically guaranteed to be isolated but not requiring actual context switches, it should be theoretically possible to create things that are structurally microkernels, but do not need internal context switches because isolation has been proved at a higher level. Or, arguably, in some sense this would be something that transcends both microkernels and monolithic kernels to become something not properly called either.
I'm sure there's many an i to be dotted and ts to be crossed before this would work, and you'd still probably want to work out a run-time loadable module which would probably make things interesting, you need a story for how a device driver can individually crash without bringing the whole process down (though since Linux can do it, presumably it is possible anyhow), and a whole bunch of things. But it does seem like an interesting opportunity for someone to make a kernel that is, well, not the same basic kernel the C type system naturally affords.
http://c2.com/cgi/wiki?NeoKernel
It's basically relying on the type system & safety mechanisms of the underlying programming language to enforce some of the isolation properties that an operating system is normally used for. The Lisp Machine was probably the most commercially successful example. Since neokernels typically require tight integration between the programming language and the kernel, there are also opportunities for efficiency gains, eg. in Lisp Machines the garbage collector was tightly integrated with virtual memory to prevent page thrashing on collection, or in modern languages you could replace the OS scheduler with promises or green threads.
The biggest downside of it is that it requires tight coupling between the programming language and OS, such that you can only use a single programming language (or a family of related ones that all share a type system) for all programs on the box. Few programming languages are flexible enough for that. With the move to cloud computing and virtualization, this becomes more practical, but then that same trend is also driving interest in the unikernel/exokernel pairing. If you only run a single application on a virtualized box, why not program directly to the hardware?
I would point out (from a relatively lay perspective) that while this isn't strictly the case in current popular kernels (Mach/OSX, Windows, Linux), it's still a pretty strong trend. These kernels (AFAIK) are implemented in C and have large ecosystems of C code orbiting them. As such there are many benefits to having a program written in C or at least speaking C's ABI and memory layout.
Maybe I'm mistaking the causes for this situation, but most developers are effectively using something that is either C itself, written in C, or speaks C in some way (CPython, JVM, MRI/CRuby, Perl, are notables that are written in C as far as I know). I think that if a language is sufficiently high performance and general purpose, it's fine for it to be the "core" language that other languages are expected to interface with.
Erlang was meant to fill this role in newer switches, but it looks like PLEX is still being developed and used.
It seems to me that recent advances in this field ought to ease the restrictions of requiring the entire stack to be the same language. It seems like a Rust neokernel ought to be able to run other programs on top much like a conventional kernel does, context switches and all. I'm not too worried about userspace/kernel context switches... there's a security barrier there that still strikes me as a good idea. I'm OK with something that produces an artifact in the end that looks like a monolithic kernel, and can function like one, and is merely internally structured with all the discipline of a microkernel.
If all kernel elements have to be Rust, well, I'm fine with that.
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?
Why not.
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 am working on some formal verification myself for some commercial projects, and I enjoy reading about stuff like this.