I would argue that it would be easier and quicker and much safer to write the kernel in a
much higher-level language like Haskell and then invest time in making the compiler and
optimiser really staggeringly clever.
It's not obvious to me that this would work, nor that if it did work it would fix a
sufficiently broad category of problems to be worthwhile, and nor that if it did work, AND
fixed a broad category of problems, it would actually take comparable time (if it takes 10
years to do what used to take six weeks then you've shot yourself in the foot because 10 years
is too late). It's also not obvious that Linux Kernel developers (often expert in C and
low-level hardware stuff) would make good compiler designers, since these are largely
No-one has, to my knowledge, been stopping people from actually developing these staggeringly
clever compilers over the decades since LISP and C were the state of the art. It's even
regarded as a genuinely interesting problem (unlike Operating systems which have been largely
treated as a commodity) so you could get funding to work on it.