[kramerger]

Warning: big piece of opinion that may trigger some of you.

In practice (feel free to verify this yourself by downloading and building the latest L4 derivative), microkernels that actually work on modern hardware need a huge amount of baseline code to get IPC and memory server working in a distributed yet somewhat performant fashion.

There is a flag for compiling Linux without any hardware and filesystem drivers. That gives you the kernel core in a surprising small binary which is not that far from sel4 or okl4.

In summary, monolithic is the new microkernel :)