On 14 Sep 2018, at 15:00, Andrew Warkentin <andreww591@gmail.com> 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).

Gernot