"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."
I'm also a big fan of Haskell, but wouldn't really want the kernel to be written in Haskell.
It's a wonderful language, and adding more static type-checking to the kernel would be great,
but for the kernel, performance should be everything (well, almost everything). I think the
kernel devs have it right: add static checks to C (via sparse).