Rust and ATS seem to be pretty well suited. With Rust getting more and more traction, maybe not all is lost :)
Redox is a ground up OS, but I wonder if we shouldn't instead be taking more of an Oxidization approach where we rewrite more and more pieces of an existing OS in Rust piecemeal. This would add some overhead (programmatically not instructionwise) of a lot of context switches though between the C and the Rust code, which is to say it would be a little ugly for a while.
It might be cleaner to go after a microkernel to do this though, like L4 or rumprun.
That's kind of the opposite of having the mindshare, IMO :) Having the mindshare means people would be reaching for it when they need things done, not have to be dragged in, and there's a wide pool of people knowing it.
I'm pretty sure you can write OS kernel in almost any language that can be compiled into runnable code, and probably if you are really determined also in those that are compiled into bytecode. As I said, it's not the main issue.
Unless you are a titan of programming that can do an OS project all by yourself, or have more money than Google, you'll need random people to come to the project, pick up pieces and work on them. The question is, does Rust have pool of people wide enough so that probability of people wanting to work on your project is higher than your needs?
C definitely has a huge pool. So do C++, Java, JS, Python and many other languages. Rust? I'm not sure it does so far. Maybe I'm wrong.
I think for its age, the success it already enjoys is impressive.
The only way I could see a kernel being truly written in Haskell is in a DSL something like atom[1]. Atom is an EDSL represents code that not only doesn't need a garbage collector, but also has a verified constant bound on memory usage. However if that's what you're looking for, you might as well go with an EDSL in a dependently typed language like Idris to make verification easier and extensible.
Some of my colleagues did, a few years ago.
I think if the Rust communtiy wants to make it somehow to the Linux (or other UNIX or windows) Kernel space, there needs to be an effort to build Kernel Rust, if there isn't one already..
Rust is popular because Mozilla, a well-known company, is developing it for a well-known major project, a web browser.
Go is well-known due to Google, and the fact that many people with an opinion-setting power know who Rob Pike is.
Haskell, well, just spent 20 years being around, sometimes in university curricula.
ATS is only, it seems, known to people who are specifically interested in formally-correct low-level code, on the sparsely-populated intersection of math and hardware geekery.
See also: seL4, Isabelle/Coq, Idris
I think solutions that don't require any code modification like Softbound and SAFEcode (and even the LLVM sanitizers) aren't popular because the resulting executables are quite slow. Whereas SaferCPlusPlus strives for minimal performance penalty. (Perhaps with some cooperation from C/C++'s formidable optimizing compilers.) (Btw, if it's not already clear, this is a shameless plug.)
And not only is conversion to SaferCPlusPlus far less effort than rewriting everything in another memory safe language, it can be done completely incrementally. What language has better "bidirectional C interoperability" than C++?
Unit testing for security vulnerabilities has been discussed to death on HN and is generally agreed that it doesn't work. Yet, every time there is any kind of vulnerability, a comment like mine shows up, except in ernest.
Look, this hasn't been a good day so far, okay?