What led us here
Microkernels, eBPF, WebAssembly, LoRa mesh and confidential computing are usually filed as five unrelated hobbies. They are one argument, running for about a decade, about where you put a boundary and what it costs to cross it.
microkernels
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 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.
