IIRC L4 is just a proof-of-concept thing to port, not necessarily what they plan for everyone to use. The Mill's security model is well-suited for a microkernel

IIRC L4 is just a proof-of-concept thing to port, not necessarily what they plan for everyone to use. The Mill's security model is well-suited for a microkernel (it doesn't have the overhead traditional architectures have with microkernels). The security model is probably the biggest thing people writing software will notice- instead of a user/kernel split with expensive transitions between separate address spaces, it's a single address space with cheap (on the order of a shared library call) transitions between arbitrary protection domains (turfs).