Go, unlikely. It's safer but it has other problems. Haskell is great but it's runtime makes it hard (though not impossible) to use in kernel development.

Rust and ATS seem to be pretty well suited. With Rust getting more and more traction, maybe not all is lost :)

I have extremely hard time believing there can be a viable OS kernel project on Haskell. I mean, yeah, you probably can write OS kernel in Haskell, if you are determined enough. But I don't believe you can make it into a viable project. Rust - maybe, if you can get enough mindshare. Which is also a big if so far...

> I mean, yeah, you probably can write OS kernel in Haskell, if you are determined enough.

Some of my colleagues did, a few years ago.

http://jfla.inria.fr/2007/actes/Presentation/tolmach.pdf

If you plan on writing your OS in Haskell in the usual sense (i.e. your OS executes pure Haskell functions and interprets some sort of IO monad) you're going to end up implementing a full microkernel in another language just to get started. Not to mention it'll be a microkernel with a GC.

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.

[1]: https://hackage.haskell.org/package/atom

I think Rust has the mindshare, what it needs is people actually doing it.

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.

> I think Rust has the mindshare, what it needs is people actually doing it.

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.

Remember, Rust is just a year old. There are already a few OS projects going in it. All the languages you mentioned are >10 years old.

I think for its age, the success it already enjoys is impressive.

It's not a criticism of the qualities of Rust. It's just an assessment of the current state of affairs. Maybe Rust will gain the mindshare in 3 years. We'll see. I personally think having something better than C but as ubiquitous and supported as C would be awesome. Is it Rust? We'll see in 5 years.

I would then say that it has momentum, not mindshare.

MkLinux was a popular environment on a portal I worked for in the late 90s. We brought dozens of Macs back into active duty as secondary workstations for the operations team.

In fact, SEL4 has parts in Haskell. The important things are all in Isabelle though and everything is compiled to C and machine code.

I played around with getting a Rust kernel module to work before. And I eventually got a "hello world" in my dmesg. But what I realized in so doing was that seemingly 90% of the higher level features of Rust were lost to my module -- essentially I got the language memory security features (borrowing and ownership) but with very little standard library help, which made the whole endeavour seem much less practical still than just using C and libc (because I would have to reimplement a lot of that functionality in Rust -- Kernel Rust, if you will).

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..

When were you doing this? There's now a large chunk of the standard library[1] that's explicitly designed to be used in bare-metal/zero-dependency situations, and it even includes "fancy" things like the formatting infrastructure[2] (it has to be hooked up to a writable/IO device, but that's just a trait implementation away) and string processing, certainly more than the zero-allocation subset of libc.

[1]: https://doc.rust-lang.org/core/

[2]: https://doc.rust-lang.org/core/fmt/

It has been at least 6 months and it's possible I just missed this! That's quite cool. Thanks! I will give this a try.

well, you can't use libc for a kernel module either :)

No, but there's 'kernel C' (not an actual/official name) with a large reproduction of much of libc ready for use there. printk() is a good example which actually has a format string implementation (https://www.kernel.org/doc/Documentation/printk-formats.txt)

right, that shouldn't be hard to map to rust I guess

Why does ATS not get more traction in discussions like this? That's what it's made for. This is the only mention so far in this comment page.

Not enough publicity, to my mind.

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.

Seriously, two things: formal verification of correctness is sorely needed and a language platform which has complete, bidirectional C interoperability in targeting both kernel- and user-land which can be gradually migrated to one compilation unit a time and has much more safety, is more succinct, has C feature parity and no/minimal runtime performance hit would be requirements for candidates to change languages, but only after impressing Linus, lieutenants and contributors of undeniable value.

See also: seL4, Isabelle/Coq, Idris

seL4 looks like a great base to build secure embedded systems on. There's an interesting project called robigalia that aims to make it possible to build seL4 userspace threads in Rust, which should be an excellent base to build on.

I disagree. It is possible to put some real effort into the compiler making the same C code safe against such problems without infinitely expensive rewrites.

Tools like this for C already exist, and have existed for some time. They've failed to reach fixation, even in security-critical areas like kernels. If that is going to be the answer, then a different approach to making C safer is definitely required.

Might I suggest SaferCPlusPlus [1] as the "different approach". SaferCPlusPlus is a memory safe subset of C++. But the key is that the C++ preprocessor is now powerful enough to enable the creation of compatible safe substitutes for the unsafe C/C++ elements. (Native pointers in particular of course.) So rather than rewriting all your code, translating from traditional C/C++ to SaferCPlusPlus can be just a glorified "find and replace" exercise. (Well, maybe a little more than that, but not much.)

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++?

[1] https://github.com/duneroadrunner/SaferCPlusPlus

Production ready tools are not there yet, they all are essentially POCs and some work has to be done to apply those ideas to existing projects. For the linux kernel, I presume, it would have to be done in gcc with a bunch of gcc flags or it won't be adopted.

The defensive tone of this comment is unseemly. C is just a tool, and I assure you, one that feels nothing for you.

I love me some C. Some of the funniest projects I have worked on have been written in C. My comment was sarcastic.

You should have mentioned the official plan of a complete rewrite as a microkernel in message-passing dialect of Visual Basic, which was supposed to land in version 3.0.

https://lkml.org/lkml/2005/3/2/247

oldmanjay did realise that ...

In fairness I haven't seen anyone make a serious comment like yours yet in this thread.

"in b4 'we should rewrite W in X/Y/Z'" has become the new "we should rewrite W in X/Y/Z".

I didnt up/down vote, but rewriting in something like a performant, secure subset of Go/Rust/X and formally-proving correctness to remove many classes of errors would arguably have immense net value greater than the pain and cost of progressive/gradual rewriting migration from C to something with fewer dangerous corners and far less code to accomplish the same system behavior.

I don't mean to show support for either the "rewrite everything in X/Y/Z" crowd or the "C is all we need forever" crowd (or their non-straw-man equivalents). I just thought the early state of the comments in this thread was funny, is all.

If anything, security vulnerabilities are precisely the kind of bugs that easily sneak by unit tests.

Try reading my comment in the most sarcastic tone you can manage.

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.

I propose a new name: a dijkstranbug. Kinda like a heisenbug except specifically for unit tests.

You had me until "MongoDB".

To be fair, there are a lot of places in the Linux kernel where primitive storage methods are used. In USB drivers, Vendor ID - Product ID pairs are stored in arrays. It's terrible and, most important, it doesn't scale. Being able to SELECT on a given VID would be really useful -- and it's really cool that MongoDB doesn't really impose too many constraints on the structure of your data.

Look, this hasn't been a good day so far, okay?

The sarcasm is strong with this one...

kernel security and later mongodb appearing randomly in a comment is like priesthood and pedophilia randomly associated. It stings of irony.