Information on implementing L4

Gernot Heiser gernot at
Fri Sep 14 07:15:05 CEST 2018

On 14 Sep 2018, at 15:00, Andrew Warkentin <andreww591 at> wrote:
> To me, language-based OSes have always seemed interesting but a bit
> impractical and limiting. A language-based OS would face more of a
> challenge when it comes to success in the real world than a
> conventional OS would (that's one reason why I'm writing an advanced
> Unix-like OS, since that is what is most likely to be used in the real
> world).

I think when you say “language-based OS” you mean type-system enforced security rather than MMU-enforced security.

I haven’t seen any approach of this sort that didn’t end up with an unsafe but trusted blob of code (language run-time) that’s as big if not bigger than your typical L4 kernel, besides having higher run-time overheads. I fail to see how this would be better in any way. Particularly when you can have your L4 kernel formally verified (i.e. seL4).

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>

More information about the l4-hackers mailing list