Well there's no hiding it, I'm a Haskell fan. GHC does support the more standard architectures
(x86, sparc, ppc - see http://haskell.org/ghc/download_ghc_682.html). As for performance, I
really think that the choice of C in general is a premature optimisation. 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
On the other hand, I'm in no way speaking from experience, so I guess like with most
academics, the world will look the other way...
Incidentally, the reason why powerful type-systems tend to only appear in functional languages
is that imperative languages just allow the programmer too much madness to permit a really
powerful type system. Scala pretty much contains everything you can get away with in an
imperative language and even there, I'm unaware that anyone's actually proved it sound.