[nickpsecurity]

Prior art includes SPIN OS (Modula 3), JX OS (Java), House OS' H-Layer (Haskell), and Verve. Each one had a type-safe, memory-safe language for implementing the features. They usually wall off the unsafe stuff behind checked, function calls. Some use VM's, too.

Ignoring performance or adoption, the main weaknesses are: abstraction, gap attacks; unsafe code bypassing the whole thing; compiler or JIT-induced breakage of safety model; common, hardware failures like cosmic rays. This is still far safer than kernels and user apps in unsafe languages.

One can further improve on it by using static analysis of unsafe code, ensuring all unsafe functions respect type-safe/memory-safe interfaces, compilers that preserve abstraction safety during integration, and certified compilers for individual components. We have production tools for all except secure, abstract compilation which (a) is being researched and (b) can be checked manually for now.