(author here) Yes, the principles described here could easily be applied to a full Linux kernel. In fact, one of the hacks on my TODO list is to statically li

(author here) Yes, the principles described here could easily be applied to a full Linux kernel. In fact, one of the hacks on my TODO list is to statically link a Mirage application against a Linux kernel (without a userspace) to run them on the bare metal. The point of defining a single address space and the smallest possible C runtime is to start from the other end: rather than stripping away 14 million lines of C code, I preferred writing a few thousand lines and jumping straight into my runtime. It is an awful lot easier to experiment with something like http://github.com/avsm/mirage/tree/master/runtime/xen/kernelthan http://github.com/avsm/mirage/tree/master/runtime/xen/kernel... the full Linux kernel by quite a long way. Note that the current tree isn't finished yet; I'm pulling out dietlibc entirely at the moment, so the final kernel binaries float around the ~200KB mark for a typical webserver. Then, also consider hypervisor-only features like live migration or PV suspend/resume that can be further optimised heavily and more easily in a minios instead of Linux. Or that Mirage is single-vCPU and event-driven only (no interrupts), and it starts to look quite different from Linux. The Mirage IO library is also very portable; an application which uses only TCP/UDP (instead of the lower level Ethernet) will compile on Linux/*BSD using select/epoll/kqueue sockets to be "just" a high performance webserver. The cool thing is that by using these APIs, we can also build applications that compile to small specialised operating systems, while developing them as usual on UNIX. For a final entertaining hack, they are also portable enough to run directly in the browser as Javascript applications thanks to Jake Donham's ocamljs project. We're still integrating the Websocket code in to make this properly finished, but it's a fine side experiment into portability :-)