That sounds feasible. I just wrote my first Rust program (search for Ruststrike in this thread) and wow it's stupid verbose and not particularly safe if put in my hands. I can see while there is determinism and fewer footguns, it painful on a C++ level to write.

I think just having less in the kernel and moving bits out (like Mach) into isolated domains is probably better than reinventing the universe for some purity argument.

Nah, an IDE was already a hell of a drug for the first levels of formalism in paradigms.. The most formal language is going to end up with a lot of transpiled code made in a combat between AI and features like a borrow checker, then once their eyes stop bleeding, the most stubborn will make it marginally better than any less formal language can achieve, then others will be able to work with just eye drops.

Microsoft are doing everything at once. Doesn’t mean it’ll stick.

Remember managed C++?