Ah yes, this oldie newsgroup post from ast, the guy whom wrote a bunch of mandatory CS textbooks and MINIX 2 (before the course moved to FreeBSD) which we had to hack on in ECS150. I’m sure he’s crazy rich by now from passive income.

A hypothetical kernel&userland like OpenBSD built on seL4 (a-la DragonFly or MINIX 3), implemented in Rust, OCaml or Haskell, with thorough unit, integration tests and perhaps formal proofs, seems like the safest, not necessarily the fastest, kernel approach possible using modern technologies. seL4 communicating by sending messages is really efficient and builds in IPC as a fundamental, low-latency operation.