What a microkernel actually costs you
The IPC objection to microkernels is fair, and it is the wrong place to stop the conversation, because what it buys you is a fault boundary that a monolithic kernel cannot sell at any price.
formal-methods
Formal methods stopped being academic
Proof used to mean a paper. seL4 shipped a verified kernel, and verification tooling for ordinary languages is now something a working engineer can point at a bounded problem.
