I think when you say “language-based OS” you mean type-system enforced security rather than MMU-enforced security
Yes, basically. I'm talking about OSes that integrate some form of language-specific VM at a fundamental level, often depending on the VM for 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).
Yes, that's basically the same thing I was saying. Managed code has higher overhead and a bigger TCB (which often contains a lot of unsafe code) than safer native code (either formally verified or just written in a safer language like Rust) does.