This approach has a few issues which make it impractical for use by a real general purpose OS:
* it moves all work related to safety either to the dynamic compiler (not so bad), when it can statically prove that the code is safe or onto the critical path if it cannot statically prove it safe (which generally causes significant slow-downs). For example a traditional OS will use VM to isolate application memory (where the performance impact comes from the occasional TLB miss), while this sort of approach might require boundary checks to be compiled before many memory instructions
* the problems mentioned above could be mostly avoided by requiring use of a language or bytecode format designed to allow the compiler to use static checks, but then all your applications have to use it (which is what Runtime.JS does)
* it potentially allows more complex interactions between the OS/VM and the application compared to traditional system calls, which is the sort of things that often enough creates hard-to-predict side effects
> allows for more easily provable safety guarantees.
I don't know about that, hardware is normally formally verified, while software normally isn't. While hardware bugs still exist, there are far fewer than in software.