Hacker News new | past | comments | ask | show | jobs | submit login
Linux Rust Support (kernel.org)
641 points by doener on July 6, 2021 | hide | past | favorite | 433 comments

It's interesting to me that there is not as much push back against Rust from the kernel. Linus (I guess everyone addresses him with his first name), has been very critical, even dismissive of systems programming languages other than C. But with Rust he has a more, I guess we could say passive approach. This might be a good indicator that Rust is doing something very respectable.

On the other hand I'm slightly suspicious of this movement. Rustaceans are very, very eager to promote the language. It would be interesting to know how much this movement comes from within the Linux kernel community or if it is driven more by the Rust community.

In any case the language seems to have potential of becoming a new mainstream systems programming language in a few years.

This is a very weird comment, of course the people driving this have a long history with the kernel... It takes about 2 minutes of using git to find out that Miguel's (the main author) first commit to the kernel was back in 2006, and that he's the maintainer of multiple different drivers.

The rust community is naturally happy to help out, but I can't even imagine us being able to drive this sort of work...

To be fair, I was just a teenager back then and I was out of kernel development for quite a few years afterwards.

But you are right, this is not coming from the Rust community itself. In fact, several independent groups have been thinking of using Rust in one way or another for kernel purposes, as early as... 2013 (!), e.g. from Taesoo Kim:

There were others: John Baublitz had a external kernel module going on, Samantha Miller also worked on enabling a FUSE-like API to write filesystems in Rust, etc. And, of course, Alex Gaynor & Geoffrey Thomas had the most mature Rust abstractions for external kernel modules.

At the moment, in the project we have a mixture of people that come from a Rust or kernel background, which has been great. And most of us have used many languages in our work, not just Rust. Personally, most of my career has been around C++ and Python.

What about it is so very weird? They cautiously raise some legitimate questions.

It has an undertone implying some sort of strange conspiracy amongst rust people. Generally to be suspicious of something means there is something nefarious going on.

It has an implication that Linux is something that any enthusiastic group of outsiders could force their changes into. And that there are rust people would create such a group of outsiders.

It has an implication that rust people and linux people are disjoint sets.

It's generally taking this strange adversarial view to a collaborative endeavour. People aren't "rustaceans" or not, it's not a sports team. People are people, they generally program in a wide variety of languages, and use whatever they think is best given a certain context.

I'm not sure if I've fully captured what seems "off" to me about the comment, but hopefully you get the gist.

As for asking questions, that's a clear example of https://rationalwiki.org/wiki/Just_asking_questions - but at the same time the general sentiment seems to be frequently reflected in internet comments. I don't think it's a malicious case of this, just how they chose to express their opinions.

It seems like legitimate questions from an outsider to me. As an outsider from both kernel and rust development myself, I also had the same questions going through my head. Specially given Linus' previous opinions in using other languages for kernel development. That, allied with how eagerly rust is hyped, does make one wonder how much is self-promotion and how much is actually the linux kernel community as a whole embracing the endevour (not just the subset of kernel developers who also happen to really like rust). I feel like they are honest questions. Someone more in touch with the kernel community should be able to answer them.

Linus’ objection to C++, if you boil it down, is that it adds a lot of complexity without fixing what’s fundamentally broken about C: memory safety. Rust’s memory model is much safer than C’s, and it is a significantly simpler language than C++ as well.

When I think about Linus’ lack of objection to Rust I immediately think about his vocal disdain for C++

When I learned rust I thought it felt more C-like than C++ to be honest. Nowadays I’m pretty happy to be in this c to rust to c loop.

I think you’re exactly right about c++ not offering much benefit to someone like Linus. It’s much simpler than c++. Rust has also informed the way I write C (granted, I’ve also gained more experience along the way, but rust forced me to have more discipline for sure).

You can't just make up stuff and go with it, you need to be a little more complete with your analysis. Especially worded the way the other comment was and your comment is, you seem to think there is some sort of confusion because you're lumping in one programming language with another and essentially saying, I don't see the difference therefore something sinister may be at play. Your ignorance is not an excuse. Either know what you're talking about or ask questions without your very, very leading premises.

Poor choice of words on my part I guess.

To clarify, I didn't mean suspicious in the sense of expecting malicious behavior, rather than in the sense of not being overly optimistic about this type of progress, because I think it is very hard to incorporate new tooling/languages despite their merits.

In other words: it would be nice to see this being fruitful, because it would possibly a strong, positive signal for programming and programming languages in general, but I'm cautious or "suspicious" still.

Please don't take my above comment too harshly by the way, I know it could be read as a list of pretty hard criticism, it's really just trying to dive into why the tone seemed off when there isn't one smoking gun. It's a list of the comment could be read like this, not that the comment actually means this.

All good! English is not my first language, plus if we all had these conversations face to face, we wouldn’t have to guess the tone.

Just fyi, your comment does come off as fairly harsh.

Thanks, I know, I wish i had at least included the language softening it in the original comment.

> some sort of strange conspiracy amongst rust people

I mean, "it seems like our technology should fit this domain, let's see if we can help them use it" isn't so strange as conspiracies go.

Honestly I think you're reading to much into this. You contributed some good points but dismissing the comment as very weird is a bit much

oh wow, downvote galore ITT. Okay, I'm checking out. This is too toxic

There is not a single question in GP's comment, let alone a legitimate one.

"first commit to the kernel was back in 2006"

That's not my definition of long history! My first Linux kernel was just pre 2.0 and I used make config. Actually I used make config for quite a while before it got out of hand and I started keeping copies of the config to work from instead of doing it from scratch each time I did an upgrade.

I'm not the sharpest tool ...

> That's not my definition of long history!

It's long in comparison to Rust!

Quite. There's a term, often used by engineers (Chartered, obviously): "time served". C is time served - it might be a bit weird and start dribbling for no reason but it quite literally runs a huge part of the world.

Rust is not time served and it needs to grow up. Initial signs are positive. We are at the cooing stage over a pretty child that may either be the Messiah (a Naughty Boy) or decide to throw its poo at its parents and stick to licking windows.

Time will tell.

> It would be interesting to know how much this movement comes from within the Linux kernel community or if it is driven more by the Rust community.

You make it sound as if those are two non-overlapping sets. I don't think they could pull off this project without intimate knowledge of the Linux kernel.

The biggest pushback was with C++. Why? Because when these discussions still started, C++ codebases tended to be a mess. It didn't help that C++11 was coming up and support was wildly inconsistent among compilers. Ultimately it was still possible to write unsafe code though.

The landscape has now changed and Rust has now positioned itself as a language that actually does have very key advantages (in correctness and safety). While C++ has made large strides, its advantages now lie elsewhere (eg; drawing on a wealth of performant libraries-- something that the kernel has less of a sue of).

Linus has been critical of C, before, too (e.g. https://lkml.org/lkml/2018/6/5/769).

If you look at Linus's criticism of C++ (e.g., https://lkml.org/lkml/2004/1/20/20), he criticizes a few specific things about the language - exception handling, implicit allocations, complex OO. Rust, as it happens, doesn't do any of that. Errors are passed back via return values (which is what the kernel already does), memory allocations are explicit by convention and "zero-cost abstractions" are favored, and the OO model doesn't have multiple inheritance or anything, just interfaces (which is also what the kernel already does, in C, using structs of function pointers).

So I'm not surprised that he doesn't have similar harsh words for Rust. It solves a lot of the issues with C that have been causing practical problems for the kernel (apart from confusing aliasing rules and confusing overflow rules, there was also the problem a while back where a bunch of != NULL checks got optimized out), and it doesn't have the problems C++ has - in fact it tends to solve those use cases in a way similar to the kernel's existing approach.

For my part, I've been involved a very tiny bit in Linux kernel development for well over a decade because I find systems programming cool, and I've also been involved a very tiny bit in Rust starting around 1.0 because I find systems programming cool. I started this project because I genuinely thought Rust would be a good choice, not because I was deeply involved with the Rust community and I wanted to evangelize it.

(I looked up the IRC logs where Alex and I decided to start working on this, and the context was that Alex had run into some bug with buffer length handling in the kernel, he was considering sending in some patches to improve the C abstractions about this, and since PyCon was the following week I semi-jokingly asked if we should instead spend our sprints time writing support to ship kernel modules in Rust. Which we did.)

The allocations thing in particular. You can watch serious C++ practitioners staring at a class definition and usage and trying to figure out answers to a quiz question, "How many allocations does this do?". Is that line a Move or a Copy? That's a bad sign for a language you'd supposedly want to write OS kernels in.

Rust got luckier here, by the time Rust was invented programmers knew they really care about this, and so Rust explicitly distinguishes Copy (this object is just bits, so you can duplicate it by copying the bits), from Clone (this object can be duplicated, but you need to call its clone() method to explicitly do that work) and gives Move semantics to all assignments of types which do not have Copy.

So in Rust "let a = b" definitely isn't doing memory allocation, it just moves bits. If you misunderstand the situation and assumed b is still valid because it was Copy, but actually it isn't, the compiler has your back and will politely refuse to let you use variable b after it was Moved. If you did still need b you can write "let a = b.clone()" and now they both still exist but anybody can see this code might be doing something expensive 'cos it calls this clone method. And if the compiler says "Ahem, you can't Clone that" then you've just learned something very important about the thing that a minute ago you assumed was just a few trivially duplicated bits.

Given that this is the kernel, using typical C++ libraries would be out of the question, so it should be easy enough to design things right from the start. C++ is after all used in embedded contexts where allocations are forbidden and it offers excellent support for this use case.

In such a project where allocations matter one would not stare at class definitions, one would ensure that there are no allocations by forbidding use of libraries like the STL and for example disabling operator new and the copy constructor. If the project is safety-critical there are tools which can enforce such rules.

Edit: I've clarified that I was referring to C++ libraries only.

Ah, I think there is a misconception at work here.

The problem isn't "Kernel code should not allocate" but "Kernel code should not implicitly allocate".

And C++ thinks this is none of your business. You can have no allocation by not providing an allocator - but you can't have no implicit allocation because the language will go out of its way to hide some of the obvious places allocation might happen rather than expose its warts.

Could you give me an example of such implicit allocations that are done by the language and would be a problem in a kernel context?

Here's my list:

* RTTI: would be disabled

* Exceptions: would be disabled

* STL, stdlib: would not be used

For example the C++ language implicitly runs constructors, which may (or may not, it depends) cause allocation, whenever it sees fit to construct any object, even if that object is temporary and will be destroyed immediately afterwards.

Now of course you could say, "Oh I never use objects, those are awful" but then you ought to ask yourself what exactly the point was of having C++ at all. Or you could say, "We'll ban constructors from allocating" but C++ won't help you enforce that rule and the resulting code won't be idiomatic C++. Implied allocation is just normal in C++.

Also note that although Rust's full standard library won't be available in the kernel, you do get Vectors, you get Rust's reference counted "smart pointer" types, Iterators, Option and Result and so on. In Rust such things don't have implied allocation, only explicit allocation which is fine.

Rust used today in the real world does have some places with implied allocation, a notable example is String concatenation. Rust won't let you write

  let hw = "Hello, " + "world";
However, the String implementation in the Rust standard library, and currently in kernel Rust, will let you write:

  let h = "Hello".to_owned(); // Now it's a String
  let hw = h + ", world";
But, that's one of the anticipated objections from Linus, and you'd just remove AddAssign (and possibly Add) from the Strings to cure it by forcing programmers to actually spell out what they want to happen here instead of acting as though concatenating strings is free.

If C++ constructors don't call allocation functions (1), don't initialize members which call allocation functions (2) and don't use features like RTTI which I've mentioned in a previous post, then they do not allocate. It's not trivial to ensure the above and while it's not usual for regular C++ projects, it's certainly manageable because C++ is used in some kernels and has a track record of being used in projects with constraints much tighter that the Linux kernel itself.

(2) seems the most tricky, but in reality, in a context like the Linux kernel where the libraries would be written from scratch or wrap existing C code, this can be controlled well. If one is including a new language in the kernel, it should be comparably low effort for example to write a custom vector container which exactly fulfills their requirements.

In the end I realize that C (and I assume Rust) makes it easier to reason about allocations in simple pieces of code which don't call functions, but this is not a deal breaker for C++ either.

So I don't think that allocations is the answer to the question of "Why Rust over C++?", as you claimed when you said "The allocations thing in particular". It's perhaps part of the answer, together with other technical reasons and personal likes or dislikes. And I believe that the latter are an important part of that answer that few if any are bringing up in this thread.

You'd need some sort of standard library, even if not the normal userspace one. The kernel has a pretty sizable "lib" directory which includes all the string functions etc. you'd expect in normal userspace C. For the Rust-for-Linux work we're using the Rust standard library's libcore and liballoc, just a slightly forked version of liballoc with the goal of getting any changes upstream once we get some experience about what works well. (Along those lines, the kernel has a non-allocating printk() that works like userspace printf(), and we provide non-allocating Rust wrappers that mimic userspace println!(). C++ in the kernel would want a non-allocating iostream, I think.)

I think you could address this point by using a slightly forked version of a C++ standard library that marked all its allocating constructors and allocating conversion functions with the "explicit" keyword. (But you wouldn't be able to upstream this, ever.)

I'm not sure if there's any other case where you'd have implicit allocations that you wouldn't be able to avoid. You may be right that this is doable entirely with library changes provided you avoid RTTI and exceptions.

One specific weird case is the copy done when capturing things into a lambda: https://godbolt.org/z/Y7fG5hjqq I expect the first allocation here because I'm explicitly calling the constructor, and that's fine, but the second one surprises me a bit, because the copy constructor is marked "explicit". Maybe people who work with C++ more regularly than me find this less surprising.

But that goes back to the problem 'tialaramex raised, about how "How many allocations does this do?" is a quiz question. Distinguishing zero from at-least-one is important, and you can do that by avoiding any heap-allocated-container types entirely, but so is distinguishing one from more-than-one.

Using Rust's stdlib isn't out of the question for the kernel, at least not the most fundamental bits of the stdlib. Rust offers a well-defined subset of its stdlib, called libcore, that is suitable for embedded work: no allocations, no OS-provided abstractions, etc. So you don't get HashMap or Vec, but you do get Option, Iterator, str (but not String, the heap equivalent), etc.

Exception handling and implicit allocations are very easy to control in C++, especially in a project where one would not use the STL or any other typical user space libraries. The language has been used in safety-critical projects and low-level embedded work for decades, so it must support such use cases well.

> Rust, as it happens, doesn't do any of that.

Rust does not allocate implicitly when you use Vec or String (or any other container) ? come on..

No, it allocates explicitly when you do that. Vec and String are heap-allocated types, so whenever you use them, you know you're doing an allocation.

In C++ you can write code like this:

    #include <string>
    #include <iostream>

    void print(const std::string &s) {
        std::cout << s << std::endl;

    int main() {
        print("Hello world!");
This compiles with no warnings, and at no point in the function "main" do you see that you're causing a memory allocation and a copy by implicitly converting your static message to a std::string, passing it to the function, and deallocating it. If you code-review "main", it doesn't look like you're doing an allocation because you're passing a const char *; if you code-review "print", it doesn't look like you're doing an allocation because you're accepting a std::string, which has already been allocated. So you get an extra, unneeded allocation in the chasm between the two, and it's very hard to track down the performance problem (or, in the worst case, a hang - memory allocation can block on flushing buffers or swapping things out, so you'd better not run into this situation in code that could itself be involved in writing to disk!).

Compare the equivalent Rust code:

    fn print(s: &String) {
        println!("{}", s);

    fn main() {
        print("Hello world!");
which produces a "mismatched types" error: "expected reference `&String`, found reference `&'static str`."

To get this to compile, you have to write something like print(&"Hello world!".to_owned()); , where you specifically instruct an allocation to happen.

The objection is to implicit allocations. Explicit allocations are fine.

> This compiles with no warnings, and at no point in the function "main" do you see that you're causing a memory allocation and a copy by implicitly converting your static message to a std::string, passing it to the function, and deallocating it

Such a warning would be a bug in this specific case as "Hello World!" is under the SSO size though - there is no call to malloc/new in this specific std::string creation.

I fail to see how that is relevant though: the kernel does not use the C standard library - it's not going to use the standard C++ library either except maybe the freestanding, compile-time-only bits such as type_traits, concepts, ...

In which case it is trivial to have a string type akin to rust's:

    class kstring {
      explicit kstring(const char* str, std::size_t len);
      const char* m_storage{};
      std::size_t m_len{};
    auto operator""_to_owned(const char* str, std::size_t len) {
      return kstring{str, len};
    void print(const kstring& str) 
      // ...
    int main() {
      // fails:
      // print("foo");
      // ok

Here, the correct answer would be std::string_view anyways (or a custom c_string_view).

> If you code-review "main", it doesn't look like you're doing an allocation because you're passing a const char *; if you code-review "print", it doesn't look like you're doing an allocation because you're accepting a std::string, which has already been allocated.

My experience really disagrees with this part, every time I've been involved in code reviews, it was common knowledge that a function taking a const& or && can cause an allocation at the call site. It's barely a beginner mistake to not take it into account.

Amusingly if you create a Vec or String that operation is guaranteed not to allocate :D

The new() functions for these types are const (ie they can be evaluated at compile time) and produce an "empty" placeholder.

Because Rust's Strings don't have NUL termination, the empty string doesn't need any backing storage, likewise for an empty vector.

When (and more importantly in many programs if) you actually add something to the string or vector that may prompt an allocation, but you called an explicit method to do that, so it oughtn't to come as any surprise.

https://github.com/rust-lang/rust/pull/84266 We have been excising this with a new opt-out mechanism so there are no allocations behind your back but the same abstractions are notheless used as the rest of the Rust ecosystem.

I'm not surprised really. The C language is pretty old, and pretty much none of the features in C++ make writing correct kernel code easier. That's not a mark against C++, it's just landed on a different niche: a high perf userspace application language for expert software engineers. Other high profile languages like Golang and Swift have a similar 'application engineer' focus that offer no meaningful improvements for kernel authors.

So it's not surprising to me that Torvalds is critical of languages that don't cater to his use case. Nor why he's less vocal about Rust. The allure of Rust is inbuilt support for multithreading, protection against data races, and an efficient memory management system.

Fine, but it is completely false that C++ offers nothing useful for kernel coding. You can see, for example, SerenityOS kernel making good use of modern features.

Any feature useful for coding libraries is equally useful for kernel coding, because the overwhelming majority of kernel code is identical to what goes in libraries, and much of it is, explicitly, library code.

People keep forgeting that ARM, Microsoft, Apple and Google OSes use drivers written in C++.

I don't think it's merely the Rust Evangelism Strike Force; Linus is notoriously critical of this kind of hype. In fact, his most vocal hatred of a programming language has been targeted at C++. Those criticisms almost surely have some amount of "lived experience" associated with them - he's not the kind of person to just buy into the hype of a programming language and risk the entire kernel over it.

Remember, this is the guy who used tarballs as a version control system up until Bitkeeper gave him free (as in beer) licenses to their DVCS. He didn't hate all version control, as much as he thought that was the case - he hated badly implemented version control, which was the standard at the time with things like CVS. That's why he ultimately wound up writing Git once the Bitkeeper deal became untenable.

In this set of old e-mails from a decade and change ago[0] he specifically calls out STL/Boost being unstable and difficult to work with, C++ providing certain abstractions that have undocumented performance problems, exception handling, and hidden allocations.

Of that list, I can think of several things Rust specifically solves relative to C++.

- Rust traits make reasoning about generic code way easier than C++ templates. In C++, you just write your template, and then the template is resolved at the site of instantiation. If it's not a valid type to put in there, then the compiler tells you that you used the template wrong, but it's still your responsibility to figure out why. In Rust, however, generic types have to be constrained with traits; which list out exactly what a generic type requires. So if you misuse a generic type, the compiler can just say 'well, you need Add on parameter T here to call this', and the error will always be on the type you used, rather than some dependent generic type.

- One of Rust's core goals is "zero-cost abstractions". It does this very well, but it also has some non-zero-cost abstractions. These I'd categorize as "transparent-and-predictable-cost abstractions". For example: Rust is known for it's borrow-checker, which provides compile-time verification of memory safety. However, these might not be the most flexible memory-management solution; so it also provides shared-ownership through reference counting. This does have an associated cost, but it's easy to reason about and clearly stated. They even provided both atomic and non-atomic reference counting options because the latter has less cost associated with it.

- C++ uses an exception handling model built around stack unwinding, which requires that all code maintain a valid stack that the C++ runtime can unwind at all times. This can pose problems for kernels which almost certainly will be doing weird things with the stack that the compiler won't entirely understand. While Rust has exceptions (called panics) and supports C++ style unwinding, it also allows you to change the exception handling model to just terminating the program instead, which matches better with how the Linux kernel handles exceptions.

- Rust also heavily discourages the use of exceptions relative to C++. Panicking is mostly reserved for error conditions that are actually exceptional (i.e. unexpected), while error conditions that are expected can be signaled using return types like Option and Result. There's even special language syntax (called Try, or the ? operator) which will automatically return if a value signals an error.

The only thing I can't say Rust solves is hidden allocations, but it seems like the plan Linus has picked is to tame that beast with a Linux-specific core library, with as much as possible mapped to Linux's existing C abstractions. This probably will work out as this is the intended way to extend existing native code with Rust libraries. (It's how Mozilla integrated things like Servo into Firefox.)

[0] http://harmful.cat-v.org/software/c++/linus

> One of Rust's core goals is "zero-cost abstractions".

It's my understanding that Rust got that term from the C++ community.

I definitely heard that expression a lot in regards to C++. That being said I would argue that Rust pushes the concept further thanks to its more powerful and expressive (if also more constraining) type system.

I don't believe that the differences which you mentioned between those languages are relevant for kernel development.

* Point one is a convenience/ease of use topic. Absent C++20 concepts or alternatively static asserts and enable_if, error messages will be harder to parse by the programmer. The one place where this may be relevant is for custom containers, but a kernel list for example wouldn't have to implement iterators and certainly doesn't need to follow the STL design which can cause hard to understand errors.

* I don't understand what you mean when you say that Rust "solves" zero-cost abstractions, but C++ has had this goal for a very long time.

* Exceptions would be disabled when doing kernel development. That being said, having exceptions in application development can be very convenient. C++ supports both, but std::optional and the like are not as elegant as in Rust.

> C++ uses an exception handling model built around stack unwinding

By default, just like Ada, C++ allows to disable exceptions and use other error checking mechanisms.

As a real life example, macOS drivers don't use exceptions.

> Linus (I guess everyone addresses him with his first name), has been very critical, even dismissive of systems programming languages other than C. But with Rust he has a more, I guess we could say passive approach. This might be a good indicator that Rust is doing something very respectable.

Or that Linus is going through something very respectable.

He still tells people off when they're being stupid. One instance of this happened a few weeks ago when an antivaxer said something on the mailing list.

He tends to temper himself a lot more though. Doesn’t seem quite as aggressive even for instance in that message.

Which is good, although I wouldn’t have minded a bit of old school Linus for the anti vaxers.

Trying to figure out how much technical merit vs. guerilla marketing hides behind a project's decision to use Rust is probably an impossible task. With Rust the two are intertwined, the language and the community have a certain militant attitude associated with them.

Looking at the complexity of Rust versus C and the very limited benefits one would get out of adding a few drops of memory safety into a sea of C, one has to conclude that technical merit alone does not explain this decision.

In any case, I don't think Linus will write another language rant after he had an epiphany about his "unprofessional" attitude. And if there's enough corporate support combined with some grassroots support, he's probably figured out that he'd lose that battle even if he were nice about it.

> the language and the community have a certain militant attitude associated with them.

I'm not even sure what this means. What do you consider a militant attitude in this context? From what I've seen, most Rust evangelists (at least here) try to explain its benefits while acknowledging cases where it may not provide something better and is instead equivalent but different or slightly worse (it's not like any language can be better in every respect).

> the very limited benefits one would get out of adding a few drops of memory safety into a sea of C, one has to conclude that technical merit alone does not explain this decision.

I don't think that's a valid conclusion, but even if it is, you haven't explained it well enough. You haven't addressed how much more complex Rust is than C no how limited the benefits would be. You've provided a tiny bit more information than "it's not worth it", which I think is far from sufficient to support that position in a discussion that can have as much depth as is easily achieved here.

> In any case, I don't think Linus will write another language rant after he had an epiphany about his "unprofessional" attitude.

It's not like he's stopped calling being stupid for acting stupid or refrained from criticizing technologies he thinks deserves it. There are recent cases (mentioned in this discussion) that outline recent cases where he's done so. I'm not sure why you would assume he's all of a sudden deciding to keep his mouth shut about what would be valid concerns to bring forth if he had them, nothing to do with interpersonal communication problems he's had in the past.

You've said it yourself - evangelism, the spreading of the Rust gospel through the act of public preaching. :-) Most technologies don't have this, thank goodness. With Rust, I always have the feeling that I'm being "sold" something, even if I may have already bought it... On the positive side, it seems to be working and Rust does have technical merit, but I do hope that the community will mellow out with time and abandon this approach of trying to prove something.

Regarding technical merit, I like to think of Rust as a C++ with switches toggled in different ways and a borrow checker on top. It's complex to think in and to write in compared to C, but it's at the end of the day much easier to write correct code in. I won't go into all the details since that would take a long time, but I hope the kernel team will write about their difficulties with Rust once they encounter them, since that should be a very fun read.

Regarding Linus, I wanted to confirm to OP that their suspicions are not unfounded, because the other answers seem a bit like gaslighting to me, especially the one claiming it's a "weird question". There is definitely more to this than technical merit, but it doesn't have to be anything ill-natured from the Rust community. My theory is that Linus' spirit has been probably broken by the corporations controlling Linux development through their many commits, his getting older and grassroots support for Rust.

> Regarding Linus ...

I wouldn't trust Big tech as far as I can throw one of their server farms. That said, I doubt that Linus's spirit is broken and he's simply surrendering to them. Assuming you aren't just ~~trolling~~ tin foil hat farming, I'll answer what I think:

I remember Linus said some years ago (probably ~2019 or 2018) that Rust or something like it in the Linux kernel is inevitable. His reasoning was that the Linux kernel is unlikely to remain maintainable in the long run. Due to the C code in the kernel being very non-standard and due to there being a lot of code in the kernel that got written the way it was for a specific reason and most of it being just unwritten implicit knowledge of the old hands. This makes it very hard to onboard new maintainers and PR's often require significant fixes and significant internal expertise to recognize the need for those fixes and be able to make them. As the old hands grow older, they may not be replaceable.

Furthermore, new bugs are now being discovered in the kernel faster than they can be fixed [1].

If I were to guess, Linus is just hoping that Rust or some other modern safe systems language suitable for kernel development (of which Rust is by far the most mature) could help sustain the kernel's maintainability.

As for why Big tech wants Rust in the kernel. I guess that's because they want total world domination. Which will probably be hard to achieve if any idiot can easily zero-day the kernel their infra all depends on and steal all their secret big data which is "the oil of the age of AI" or rootkit a phone making it harder to surveil it's ~~owner~~ addict. ;-)

> Regarding technical merit ...

Rust is very fundamentally different from "C++ with switches toggled in different ways and a borrow checker on top". I could call Java "Cobol with switches toggled in different ways and inheritance on top" but that wouldn't make them quite that similar as I've made them sound. If you think that Rust isn't fundamentally something drastically different from C++, you either don't have a clue about C++ or don't have a clue about Rust. Rust is holistically designed to be safe, which is the only possible way to actually make a safe language. C++, however modern and with whatever programming best practices and tools, is still fundamentally completely unsafe. It helps reduce security vulnerabilities from very very very unacceptably high to merely very very unacceptably high but in this case better is nowhere near good enough. Rust actually eliminates entire classes of security vulnerabilities (with some manageable caveats).

Another difference is that by the time you've addressed all the reasons typical C++ code is unacceptable in a kernel, you are back at simply C. But you can have high level abstractions and safety and, etc. in Rust inside the Linux kernel. For just one difference, Rust's zero-cost abstractions are actually, you know, zero cost. Unlike C++'s supposedly zero-cost abstractions which have unacceptable (in the Linux kernel) overhead. (For example a move in C++ is potentially very expensive, but at worst it is a memcpy in Rust.) But there are plenty of other reasons mentioned in this thread.


I wonder why Linus would think that though, because when one considers how big the kernel already is, and that in e.g. 10 years the vast majority will still be written in C, which will be just as unmaintainable as it is today if not more and that those old hands will be even older... the inescapable conclusion is that the Linux kernel will become unmaintainable period.

I'm skeptical that introducing a new language, whatever that may be, would help. In the short term it will make things harder, since maintainers have to juggle two languages and in the long term, as long as the new language does not displace the old one the situation would not improve.

Past related threads (may be incomplete):

Rust heads into the kernel? - https://news.ycombinator.com/item?id=27248059 - May 2021 (179 comments)

Linus Torvalds on Rust support in kernel - https://news.ycombinator.com/item?id=26831841 - April 2021 (290 comments)

An RFC that adds support for Rust to the Linux kernel - https://news.ycombinator.com/item?id=26812047 - April 2021 (261 comments)

Supporting Linux kernel development in Rust - https://news.ycombinator.com/item?id=24334731 - Aug 2020 (354 comments)

Linux kernel in-tree Rust support - https://news.ycombinator.com/item?id=23800201 - July 2020 (491 comments)

Linux kernel drivers in Rust might become an option in the future - https://news.ycombinator.com/item?id=20833639 - Aug 2019 (254 comments)

It seems like this now has enough momentum and strong industry support to actually happen.

With the initial announcement I mentioned that Linux will need quite a customized Rust experience, and was hopeful that this effort could improve the situation for everyone.

It's great to see this actually happen, with changes already flowing back into core and alloc.

A lot of progress in just a few months!

> With the initial announcement I mentioned that Linux will need quite a customized Rust experience, and was hopeful that this effort could improve the situation for everyone.

My small contribution to this, https://github.com/rust-lang/rust/pull/84266, is supposed to be just that!

Neat. Is anything needed to disable SIMD in rust libcore? Maybe with this style of feature flag, core can maybe finally start using SIMD properly (conditionally)?

Working on a proposal to shore up opt-out feature so the stdlib can use them without fear, rather than the stop-gap ad-hoc CFG tokens the PR used temporarily.

Are there any other devs who think this might be what enables them to contribute to the kernel? I've always felt like there's this enormous mountain of knowledge I'd have to know to implement the smallest feature in the kernel:

- C pitfalls, probably documented all over the place.

- C idioms. These are hard to locate for most languages; I wouldn't know where to look in case of C.

- Kernel-specific C idioms. This is probably easy to locate and well documented, but I'd still expect it to be several thousand words.

- Code formatting tools. Are there any canonical formatting tools for C, or is it fragmented like for most older languages?

- How to test C code, which IIRC requires jumping through quite a few hoops.

- How to deal with text, which is a nightmare outside of ASCII in most languages.

None of that is specific to C except maybe the last one when compared to Rust.

1. Rust has pitfalls

2. Rust has idioms

3. Rust in kernel would have specific idioms

4. clang-format and uncrustify are two solid choices

5. Nothing is special about C that would make testing hard.

1. Yea, a road that was used for target practice during a large-scale NATO training exercise is the same as a road that could do with a bit of maintenance with painted potholes to warn people. After all, they both have potholes.

2. You are cherry picking. He also said "These are hard to locate for most languages; I wouldn't know where to look in case of C." Rust has some advantages from for example Clippy and from a very newcomer-welcoming and helpful community.

3. Rust in kernel would indeed have kernel-specific idioms. But it'll probably be very similar to other embedded Rust and relatively easy for a newcomer to pick up. (Ee'll have to wait and see, but there is good reason to expect this.) C in kernel is known to be very hard for other C developers to pick up.

4. Thanks for the info.

5. But some things are special about Rust that makes testing easy.

6. The kernel doesn't deal much with text and even when it does, it generally doesn't need to deal with encodings (let alone modern encodings). That said, text is really a nightmare in C. Even just ASCII is needlessly complex due to null-terination, badly designed functions and the regular C UB pitfalls. At least you did acknowledge it may indeed be a problem for C compared to Rust.

I think the commenter you replied to meant that they know Rust a lot better than they do C, which makes it easier, particularly since C has such a long history.

  We have been in contact with a set of companies and academia members
  that would like to use Rust as a second language in the kernel. Some
  of them have already started to evaluate Rust for their needs using
  the infrastructure we have already in place.

  In particular, we have got a few statements from major companies.
  In no particular order:

    Microsoft's Linux Systems Group is interested in contributing to
    getting Rust into Linux kernel. Hopefully we will be able to submit
    select Hyper-V drivers written in Rust in the coming months.

    Arm recognises the Rust value proposition and is actively working
    with the Rust community to improve Rust for Arm based systems.
    A good example is Arm’s RFC contribution to the Rust language which
    made Linux on 64-bit Arm systems a Tier-1 Rust supported platform.
    Rustaceans at Arm are excited about the Rust for Linux initiative
    and look forward to assisting in this effort.

    Google supports and contributes directly to the Rust for Linux
    project. Our Android team is evaluating a new Binder implementation
    and considering other drivers where Rust could be adopted.

  In addition, IBM contributed the Rust kernel support for PowerPC
  which was already included in the RFC.

Funnily similar wording to an old slashdot troll message about rewriting the Linux kernel in Visual Basic:

“I hope to see a switch from C to VB very soon. I've already spoken with various luminaries in the C coding world and most are eager to begin to transition. Having just gotten off the phone with Mr. Alan Cox, I can say that he is quite thrilled with the speed increases that will occur when the Linux kernel is completely rewritten in Visual Basic. Richard Stallman plans to support this, and hopes that the great Swede himself, Linux Torvaldis, won't object to renaming Linux to VB/Linux. Although not a C coder himself, I'm told that Slashdot's very own Admiral Taco will support this on his web site. Finally, Dennis Ritchie is excited about the switch!”

Did Netcraft confirm it?

> Microsoft's Linux Systems Group is interested in contributing to getting Rust into Linux kernel. Hopefully we will be able to submit select Hyper-V drivers written in Rust in the coming months.

At very least the Azure Sphere OS team should finally adopt Rust, instead of doing security marketing with the 7 layers of whatever, and then shipping a C only SDK.

It is like they are absent of the company security efforts, while trying to sell us a story of how much they care about security.

Azure Sphere OS was designed to fit in a 4MB of SRAM envelope... while actually using a Linux kernel.

If I remember well, only 512KB is actually usable by OEM applications on that platform.


I was using C++ on MS-DOS.

Not even C++ is supported on the Azure Sphere OS SDK.

Ironically they usally tend to evade the question when asked about it, to the point they ended up writing a very long blog post trying to justify C, and it had nothing to do with space requirements.

Rather industry expectations and other marketing speak.

The libc and libraries that they already add to apps don't leave enough space for an off-the-shelf C++ runtime to be included.

So instead of including a custom runtime they just bailed out...

And? Turbo and Borland C++ also had their off-the-shelf C++ runtime to fit into either 64 KB COM files or up to 512 KB memory space with EXE.

In fairness, back then C++ was a much smaller superset of C than it is now.

Same applies to C.

Anyway just search for Jason Turner's talks on targeting Commodore 64 with C++.

Not really. That is, C's libraries grew less than C++'s libraries, over the past 25 years or so.

Do you use everything on the standard library? Uau.

Also people are using glibc++ on avr micro controllers.

So they are not using RUST because it is bloated but for other will be ok to use it. Linux kernel is already quiet bloated so i don't see what rust can bring. BSDs start looking more and more interesting.

> So they are not using RUST because it is bloated but for other will be ok to use it.

No. They are only using C. They are not using anything else for "unknown" reasons.

You can write bloated Rust applications in pretty much the exact same ways you can write bloated C applications (generics, runtimes, macros, ...).

And you can write thin Rust applications in pretty much the same ways you can do so in any other language, including C.

Tangentially, on what parameters is the linux kernel bloated?

I presume it's mostly that the kernel ships so many drivers.

A huge number of them is in the form of downloadable modules, that is, if you don't connect the hardware, the relevant module isn't loaded.

It is better when others have skin in the game and you are protected from risks. The fool doesn't learn from his own mistakes, the smart one learns from his own mistakes, the wise learns from the mistakes made by others. Very wise Azure people are. :)

Obligatory "The S in IoT stands for Security"

I never quite understood why Ada/Spark dont get the same attention or love.

IMHO, Ada missed its chance to shine when it didn't have any satisfactory FLOSS build chain right at the time that paying for a compiler became a thing of the past.

I think you may be right, but it's disheartening that this essentially boils down to a failure of hype.

Ada may be a good language, and GNAT may be a fine Free and Open Source Ada compiler, but Ada isn't a new programming language. Software developers only chase shiny new things. Ada is held back by its beginnings as a niche language with expensive compilers, it doesn't matter that this hasn't been the case for decades now.

Don't undersell that programming is tribal, and any language that deviates too far from the C/C++ syntax (from the ALGOL mold, that is) will constantly be fighting against what people consider the "norm" and those preconceptions. The closer the language is targeted at something that C and C++ are still commonly the main choice for, the harder it will be to get some people to consider an alternative if it using different syntax or structure in any way.

I think one big stumbling block people had in adopting ADA (along with there not being a good open source toolchain for a long while as noted here) is that it just looks different to people that primarily use C and similar languages, and that puts some people off.

That's sad, and I would rather it not be true, but it's become increasingly obvious to me from how people treat numerous newer languages I've seen pop up over the years.

There are plenty of very successful languages that look nothing like the C family. I think the syntax of ADA has a different issue, which is that it- to me at least- evokes languages that are considered old fashioned or out of date like BASIC/Fortran/COBOL.

I'd be more than willing to give Ada a chance, but when I looked at code samples I definitely had to fight an automatic response of thinking it was something out of date based on how it looks.

> There are plenty of very successful languages that look nothing like the C family.

It's not that there aren't successful languages and have a different look and feel, it's that there's pushback against them when they are targeted towards the niches C and C++ are already strong in. Obviously many languages exist and many have become popular, but certain niches are more resistant than others and sometimes it's for non-rational reasons.

> I'd be more than willing to give Ada a chance, but when I looked at code samples I definitely had to fight an automatic response of thinking it was something out of date based on how it looks.

That's part, but not all, of what I'm talking about. The style C follows is damn old itself, sometimes predating the languages you're thinking of as out of date.

> it's disheartening that this essentially boils down to a failure of hype.

Maybe also, but not only. In contrast to Rust, Ada docs have been awful, and as long as you didn't get a commercial toolchain you had to play with some gimped version (and the really free version didn't come out until the language was 20+ years old), the build system was as “good” as C, people complain that Rust is verbose, but Ada was still a notch over, the memory model of Ada is a mere reflect of Rust's one, and (maybe I'm being subjective here) Rust's stdlib and philosophy is leagues over Ada's (Option, Iterator, closures, Result, ...).

Ada had the potential to be a Rust 30 years before, but it was never the goal of its owners.

> it's disheartening that this essentially boils down to a failure of hype.

That kind of thing happens; we're in a profession that is made up out of people.

Quiet frankly, they solve different problems. Ada includes a GC as part of the runtime and can still run into memory safety issues if you don't use the GC.

Rust has opt-in memory safety issues but outside of those, does not require a GC.

Rust does not have Ada's constraint system. In that way, rust is easier (and arguably less safe) to program.

Ada didn't get the same love as Rust for the same reason D goes pretty unloved. The problem systems engineers needed solved was memory safety without a GC. Neither D nor Ada solve that problem.

This is incorrect, Ada's spec leaves open the possibility for GC, but none is mandated or even used AFAIK. The GNAT runtime is non-GC.

Right, but (not counting extremely recent work that's directly inspired by Rust and therefore necessarily less mature than Rust's implementation) when you use Ada without a GC, you either have to avoid dynamic allocation or use Unchecked_Deallocation, which lives up to its name.

Static memory allocation is totally fine if the thing you're building is, like, a control system for a jumbo jet. You know exactly how many engines you have, how many wings you have, how many pilots you have, etc. Your autopilot has a fixed set of parameters: heading, speed, altitude, etc. You know exactly what tasks you're running: watch engine performance, watch the altimeter, watch cabin pressure, find the instrument landing system and line up with it, etc. If you have some new instrument to plug in, you get a new version of the flight control software, and you're certainly not plugging in new things mid-flight. Even if you aren't running all the tasks at once - e.g., you're usually not landing the plane - you want to guarantee you could turn on any of those tasks. You never want the possibility of running out of memory when you try to land, so you want to allocate memory for landing the plane at design time that's always reserved for landing the plane, and nobody would call that a "memory leak."

A general-purpose OS like Linux is different. You can create as many processes as you want. You can mount as many filesystems as you want, of various formats, whenever you want. You can plug in devices while the system is running. You can add drivers to a running kernel and remove them too. You can configure network connections, turn swap on and off, etc. Inbound network connections can show up at any time. So it needs dynamic allocation.

Ada is fantastic for problems like a flight computer. But it's a different sort of problem. For a general-purpose OS, you are allocating and freeing things in response to user input, and you want to make sure you neither leak memory nor use memory after it's been freed.

Rust is very good at solving that specific problem without the need for a GC. That's what people mean when they say "Rust doesn't use a GC."

Memory safety without a GC.

AFAIK short of SPARK:

* Ada has pointer arithmetic, you can overflow buffers or read out of bounds.

* Dynamic allocation is straight unsafe and unchecked (unless you have a GC, in which case… you have a GC), you can use-after-free and double-free if you copy pointers beforehand.

* Accessing uninitialised variables is not forbidden.

* You can dereference null pointers (though it should cause an exception so I guess that's memory-safe).

> * Ada has pointer arithmetic, you can overflow buffers or read out of bounds.

Not true. Arrays have bounds and those are checked. However, you can do arithmetic with the type ptrdiff_t of the package Interfaces.C.Pointers. You can also do an Ada.Unchecked_Conversion on a pointer that you get from a C function. Obviously that's unsafe.

> * Dynamic allocation is straight unsafe and unchecked

If allocation on the heap fails, it will raise a Storage_Error, but you can catch it. Also, the language has a lot of restrictions on when you may copy and store a pointer.

> * Accessing uninitialised variables is not forbidden.

True, but there are pragmas like Normalize_Scalars (to initialize them to invalid values) or Initialize_Scalars.

> * You can dereference null pointers

True, but dereferencing will raise an exception. Also you can define non-null pointers like this:

    type Foo_Ptr is not null access Foo;
or add a "not null" constraint to a nullable pointer type:

    procedure Bar (Value : not null Foo_Access);

Ada syntax is too verbose.

Ada deliberately places readability before writeability. It's interested in the maintainability of large mature programs, and isn't intended for rapid application development.

I don't have enough experience with Ada to comment on whether its verbose and keyword-heavy syntax succeeds in this goal.

Ancedotally, I agree with zerr's comment below. Its generally not the syntax/keywords that make code hard to read, or easy to maintain. If you're familiar with the language, you learned to parse those basically sub-consciously.

For me, its always the var/function names and comments that determine how readable a program is.

Code is not a prose. C-like syntax is much easier to read compared to Ada/Pascal's text blobs.

According to studies which we have none of right now.

So that's like... your opinion, man.

Besides, if the prose would have been preferable over symbols, we'd be writing e.g. "an unknown number of apples summed up with an unknown number of pears equals to one hundred entities" instead of "x + y = 100" in math classes :)

That's a caricature. We sometimes use words for summation, e.g. Python's sum and fsum functions. I do wonder though if people had to write like that before the development of modern mathematical syntax. Even the '=' symbol is relatively young. Wikipedia tells me it was invented in 1557.

SQL is another 'wordy' language. There are many, many things wrong with the SQL language, but I wouldn't say its wordiness is one of them.

Every one of these companies except has a competing OS. Just saying.

Having Linux make the first move, then learn from their successes and mistakes to implement a better version in your own OS seems like a good move that profits everyone.

It's not like Microsoft isn't pushing Rust on their own platform. Every time a Windows driver does a use-after-free somebody swears at Microsoft for causing a bluescreen.

From what I've heard (3rd hand :D), Rust has already made it's way into the windows kernel.

All of them are interested in good technical security (actually being secure).

So why not formal verification or static analysis tools of an existing codebase (Frama-C)? Or dropping in C derived from a formally verified source (Idris / F-Star)? Or a language with good performance and a verified subset (Ada/Spark)?

I've never read anything to make me think that Rust is a safer alternative than any of these options; the guarantees of the language are just assurances of its advocates.

Its not like Microsoft does not work on that, they probably have a dozen different formally verified programming languages around at the moment. You already mentioned F*[0], but there is also Checked C[1], VCC[2], koka[3], dafny[4], Project Verona and probably some more that I am missing. The point being that they have clearly evaluated and have used F-Star for parts of the OS already.

[0]: https://www.fstar-lang.org

[1]: https://www.microsoft.com/en-us/research/project/checked-c/

[2]: https://www.microsoft.com/en-us/research/project/vcc-a-verif...

[3]: https://github.com/koka-lang/koka

[4]: https://github.com/dafny-lang/dafny

[5]: https://www.microsoft.com/en-us/research/project/project-ver...

As one of the developers of this patchset, here is my simple answer: try it. I'd love to see it.

I know Rust; I don't know Frama-C or Idris or Ada. What little I know of Ada indicates that it doesn't actually solve the problem because it doesn't have safe dynamic memory allocation. Ada advocates have told me I'm wrong and there's some new thing (inspired by Rust) that does this. Maybe! I'm not sure there's any benefit to the world in arguing it; someone skilled in Ada should just write something and show how it would actually work.

Write a kernel module with any of those techniques, send in a patch, and see what people say. Any effective means of making the kernel less buggy is great. It doesn't have to be Rust.

I claim that Rust is effective because, well, those patches are there, and frankly I haven't been doing any work for this project in almost a year and we're getting so many enthusiastic contributors. So, apparently, a lot of other people also know or are willing to learn Rust. Maybe it's actually better than the alternatives you mention; maybe it just has better documentation. I don't know. I'm not claiming Rust is perfect, just that it's empirically likely to solve the problem.

If you can get together a community of folks who can do any of these other approaches, that would be fantastic. Try it!

> What little I know of Ada indicates that it doesn't actually solve the problem because it doesn't have safe dynamic memory allocation.

It does, just not the way most are used to it.

Surely if one wants to code like malloc()/free(), free() is unsafe in Ada and requires the Ada version of unsafe {}

However many type constructions in Ada do dynamic allocation by themselves, including on the stack.

If memory allocation fails, an exception is thrown and a retry with less memory requirements is a possible execution path.

Ada also has RAII since Ada95 (controlled types), and yes SPARK formal specification now allows for ownership rules.

> If memory allocation fails, an exception is thrown and a retry with less memory requirements is a possible execution path.

So, since we're talking about the Linux kernel, that's a red flag straight away. Notice a whole section of this new LKML post is about their implementation of Rust's alloc crate? Linus doesn't want useless exceptions here and has previously objected on that basis.

Meanwhile... Over in the C++ world they have this same behaviour. For them these exception handlers are a fiction, in reality popular standard libraries (never mind everything else you're using) will blow up in low memory and it's game over. Maybe Ada does a lot better. Maybe.

Linux kernel doesn't have clearance for high integrity computing, or being in control of machines responsible for human life's, Ada does.

Ada also has no exception allowed profiles and other mechanisms.

HN is not the place to hold a lecture on Ada features.

It is not a maybe, rather lack of knowledge.

You seem to be arguing as if this effort should have gone to Ada instead. So go ahead and do it. There's a group of people who are trying to get kernel support for Rust. This is not a statement about Rust being superior to Ada or Ada's (in)suitability for the same job. It's only a statement that this group of people likes rust for it's safety features. I'm sure they are all aware that there are other, even safer languages, but these people like Rust.

We can lead academic discussions about which language is safer/better/leaner/whatever-er, but the fact is that Rust has a larger and growing mindshare so this effort is unsurprising. For Ada, the solution isn't to try and prove to anonymous forum goers it would've been better choice if only people recognized the fact. The solution is to mobilize the Ada community to put the same amount of effort into the publicity and marketing (yes, the bad M word) of their ecosystem.

Ada clearly lives on in many safety critical systems, but judging by the admittedly biased topic frequency on HN and other technical sites, it has a tiny community who mostly keep to themselves. That's fine, but then don't be surprised when it's Hip Language X that gets the headlines and these sort of efforts.

That effort has been happening for production code in high integrity systems since Ada was released to the world in 1983.

My only point is how many in the Rust community advocate as if Rust would be the first language having features, that actually were already in Ada for the past decades.

As for Ada on Linux, naturally Linus would never go along it.

A C kernel guy liking a language with Pascal syntax, a community that worships a paper that hasn't been true in the Pascal world since early 80's, not even at gunpoint.

If you want to see a use case where Ada was chosen against Rust, check NVidia's project for self driving vehicles firmware.

I appreciate what you are saying, but it is again just repeating why Ada is better than Rust. I posit that's irrelevant to this discussion. Rust is a safety centered language that seems to have champions and a growing community around it. Can we not just be happy that finally a safety conscious language has a following? If you are convinced Ada is better, nobody is stopping you from being the champion and building the Ada ecosystem. Right now, Ada is for all intents and purposes invisible both in terms of libraries, mindshare and hype.

Ada is alive where it matters most, high integrity systems.

Plenty of safety conscious language have had followings since ALGOL, this is the point that many miss when praising Rust, while ignoring our computing history.

>the fact is that Rust has a larger and growing mindshare so this effort is unsurprising.

I think that is a false perception created by the dev-blogging community. Based on GitHub activity (https://madnight.github.io/githut/#/pull_requests/2021/2) Rust usage is declining (absolute numbers show little growth). Based on developer surveys (https://www.jetbrains.com/lp/devecosystem-2020/) very few people use rust outside of hobby development.

I think the concern is that the core argument that "I think Linux should adopt rust for safety" is a bit dishonest, given that there are a large number of well-vetted alternatives. "I think Linux should adopt rust because I like rust for social reasons" would probably be more correct. That Google staff seem to think rust is good for the Linux kernel but not, say, Zircon, would be surprising if those same people actually believed that any legal rust program is safe and inherently trustworthy. "Embrace, extend, extinguish" wasn't that long ago.

I don't use rust so I have no money in this game, but based on the two links you provided, Rust ranks the highest among the "safety minded" languages. It ranks the same level as Ruby, Swift, Matlab or R in the Jetbrains ranking. That's incredible for such a new language.

I mean, neither Ada nor Zircon are even on the lists, so in terms of mindshare, they are clearly blown out of the water by Rust (from the evidence you provide). To discount Rust based on usage when the alternatives being suggested don't even make the rankings is also a bit dishonest.

In fact, the argument "I think Linux should adopt rust for safety" makes perfect sense. Here's finally a safety conscious language that seems to be embraced by a larger community, and even the big tech players. Instead we get people suggesting arcane alternatives that may be technically better, but have a snowball's chance in hell to become commonplace any time soon.

Zircon is a kernel.

That’s minor. It sounds like you agree with the rest of the post?

Rust was considered for Zircon. The only reason it wasn't chosen was that at the time Rust wasn't yet sufficiently mature for embedded. And it really wasn't.

In the meantime, Google makes extensive use of Rust in new components of both Fuchsia and Android and even rewrites some legacy components where it makes sense.

Right. It is a lack of knowledge, and I know I've seen you argue that Ada has facilities for this before, and I don't know enough Ada to answer that one way or another.

I think you and 'grumblenum should team up and write a working kernel module in Ada/Spark and then we can have a fruitful discussion about it, instead of just theorizing about whether it could be done. I'm interested in seeing the problems solved, and I'm indifferent to technology. If you think Ada/Spark can solve them, that would be awesome!

(Editing to reply to a small claim in another subthread, "Linus would never go for it" - we believed the same thing when we started. We were originally thinking that we'd pitch this directly at Linux distros shipping out-of-tree modules that they didn't want to keep having to push security updates for. https://github.com/fishinabarrel/linux-kernel-module-rust was out-of-tree and we tried to keep compatibility with kernels 4.4 onwards. But it turned out Linus isn't opposed to it.)

Fascinatingly, the more you post, the less convinced I am that Ada could ever be suitable for this use case. I looked at all these links to see what's been done:

Muen: If I am reading the allocator in https://git.codelabs.ch/?p=muen.git;a=tree;f=tools/liballoc/... correctly, it simply has no deallocator function at all. It does have a "Clear" function, but there's no sign that it has any ability to statically check that calling it is safe. That is exactly what we're talking about.

Nvidia: No public source code, and it's not obvious what actually exists here, beyond a compiler to Nvidia hardware.

Genode: This project is mostly written in C++. There is a very tiny, experimental amount of Ada in it (< 400 lines of code). There's certainly nothing that speaks to the questions discussed in this thread (safe dynamic allocation/deallocation, security, etc.).

ApexAda: This is a marketing brochure. Also this marketing brochure talks about "significant deployments in satellite communications, avionics, weapons control systems, and a myriad of other mil/aero applications," all of which - as discussed elsewhere in these comment - are applications that neither need nor want dynamic allocation (and are generally not exposed to deeply-structured untrusted input, for that matter).

Green Hills: This looks interesting - there's a POSIX filesystem and a UDP socket implementation, both of which (probably) want dynamic memory allocation. That is, at last, an application that needs dynamic allocation. Is it actually written in Ada? I see that the RTOS itself supports development in C, C++, and Ada, and they claim to offer a BSD socket implementation, so they at least have C bindings. I don't see any claim about what language it's written in, and Green Hills seems to do a lot of C work (see e.g. https://www.ghs.com/products/micro_velosity.html). If it's in Ada, then I think this gets the closest to what would be needed for the Linux kernel - do you know how their filesystem and socket implementations handle dynamic allocation? (I'll also note that they lost their certification many years ago, so if the answer is that they have safe code because they spent a whole lot of time perfecting a single version of an OS, then that's a very different problem space from Linux, which is constantly changing.)

Wind River: This is a marketing page without much detail, but it looks like it's a hypervisor to run general-purpose OSes on top of, not a general-purpose OS itself, which means it probably does not need dynamic memory allocation, or that if it does, the safety of deallocation can be verified by hand.


No Ada developer has done what's being done in this patchset, and it's pretty insulting to the folks putting in the work to claim it's been done and Gish-gallop a bunch of random links and expect people to put in the time to figure out what exactly you're claiming already exists. Everyone knows it's possible to write code in Ada. Nobody is asking if Ada can be used for completely unrelated purposes. You may as well link to GORILLAS.BAS and ask why the Linux kernel isn't using QBasic, a memory-safe language if you use the subset without PEEK and POKE.

Write - or point to - a kernel driver for a UNIX-like operating system written in Ada, that safely handles dynamic allocation. That's the clear bright-line goal. If you think that's not the right goal, say why.

>I'm interested in seeing the problems solved, and I'm indifferent to technology.

I think the first problem is some kind of language specification. That it's not possible to know what behavior one should expect from rustc means that it isn't a solution. It's another problem. You should check out Ken Thompson's great speech on why this is an issue. https://www.cs.cmu.edu/~rdriley/487/papers/Thompson_1984_Ref...

Or do you think it's wrong to regard unauditable enhancements to free software paid for by Google with suspicion?

Ken Thompson's speech was made two years before the first draft specification of C was published, so I don't understand how it is connected to language specifications.

Here's a way to address the issue he brings up in that speech that does not involve language specifications: https://dwheeler.com/trusting-trust/

As one of the developers of this patchset, can you comment on how these contributions will be licensed? Can you also comment on how a third party can verify or audit the output of a compiler without a specification?

>just that it's empirically likely to solve the problem.

Can you comment on what empirical evidence you based this statement on?

> As one of the developers of this patchset, can you comment on how these contributions will be licensed?

Yes, I can comment on this. The licensing is the same as any other submission to the Linux kernel. See https://www.kernel.org/doc/html/latest/process/license-rules... for Linux kernel licensing in general and also https://www.kernel.org/doc/html/latest/process/submitting-pa... for the meaning of the Signed-off-by lines.

> Can you also comment on how a third party can verify or audit the output of a compiler without a specification?

I imagine it's pretty similar to how you verify or audit the output of a compiler with a specification. If you can show me an example of the sort of verification or audit you envision, I can perhaps give you a more helpful comment.

We do not make any claims about verified or audited compiler outputs or compliance with specifications, and to the best of my knowledge, the Linux kernel does not currently verify or audit any compiler outputs, so I'm not sure I follow why I would be particularly qualified to comment on it, but I could maybe point you at some interesting research.

> Can you comment on what empirical evidence you based this statement on?

Yes, I did comment on this, in the paragraph you quoted. If you'd like me to expand on something can you clarify?

>I imagine it's pretty similar to how you verify or audit the output of a compiler with a specification.

I must be missing the humor here. You can test against a specification to verify implementation. Testing an implementation against itself is meaningless. I would think that this is obvious. Also I don't typically use the word "empirical" to indicate purely qualitative assessments or intuition. You also provided a dead link.

Fixed the link, thanks.

There's no attempt at humor here - I'm just trying to get you to explain what, precisely, you mean by "test against a specification to verify implementation" so that we're in agreement on terms.

When I hear "test against a specification" and "verify implementation," I think about things like CompCert. But the Linux kernel does not use CompCert, it uses GCC or Clang. To the best of my knowledge, neither is tested against a specification and neither has a verified implementation.

Actually, when we first started discussing mainlining this, we had a bit of discussion about whether it was safe to allow rustc-compiled Rust code to link against GCC-compled C code. The specific worry was potential compiler bugs, of which the kernel has historically run into many. We eventually decided the risk was low, but the kernel has gone through periods where it insisted you use the exact same compiler for the kernel and for modules because of bugs. Those bugs have gone away through the normal human process of writing better code, not through formal verification. And when they existed, the kernel's response was not to reject those compilers, it was to work around the bugs.

Also, CompCert does not test against the C standard, which is written in English prose. It tests against the CompCert developers' attempt to re-express the C standard in terms of machine-checkable theorems. The C standard is confusing even to human readers, so it would be misleading to say that CompCert has verified their compiler against the standard as published by the standards committee. (Hence my claim that they're similar; you can verify a compiler of any language provided you write your own machine-checkable statements about what you expect it to do, and you still need other humans to read those theorems and convince themselves that they're the right ones.)

For those reasons, I'm trying to understand what your question is in a precise manner. Are you asking about things like CompCert? Because if so, I don't follow the relevance to our work, though again, I'm happy to point you at interesting research.

Without being an expert in either language, given what Ada is used for, I'm sure it offers at least all of the safety Rust offers and probably more.

But Rust has a lot more going for it than safety. Maybe it shouldn't matter for kernel code, but the focus on developer "ergonomics," high-level functional constructs and pretty flexible pattern matching, supporting both ML-style and Algol-style syntax, very strong language-level tooling for building, testing, packaging, and generating documentation, plus the fact that the language itself is so well documented with great, accessible tutorials.

There's a reason it keeps winning Stack Overflow's most loved language award every year. It's easy to learn for people coming from almost any kind of programming background, supportive of newbs, and equally well-suited for application-level and system-level development, so it ends up with pretty widespread appeal.

So again, I don't know that any of this should matter for selecting what languages you're going to support in the kernel, but as a purely practical matter, it's a lot easier to ask contributors to use a language they already know and use elsewhere than it is to ask them to learn something new that they don't use anywhere else, which is what Ada and Idris and what not would be for most developers.

Rust has far more enthusiasm from potential contributors than any of those options. Onboarding something is meaningless if it's not going to be used and maintained.

FWIW I would trust anything language-level over applying static analysis tools to C (for an evolving codebase like Linux, having the safety be a first-class part of the codebase is a must) or extracting C from another language (the semantics of C are surprisingly weak, such an extraction can only ever be as good as your model of C which will probably be buggy).

> I've never read anything to make me think that Rust is a safer alternative than any of these options

What Rust focuses on is providing a scalable approach to a limited kind of formal verification - focusing purely on type- and memory-safety, not conformance to arbitrary specifications. The latter is of course being worked on, but type safety and memory safety are table stakes.

So what is the issue with Ada/SPARK?

I can't think of a case of a system like that being revived after 10 or more years. My best guess is that the mismatch between the environment the language was written in and the modern world simply becomes too great for anyone to care after a while.

For instance, I have to deal with JSON. There's no reason older languages can't deal with JSON, but it'll often be inconvenient as the libraries try to deal with mismatches in the type system or whatever, and it just can't ever be quite as slick as a more modern language written with some partial, vague combination of the fact that JSON exists in mind, together with the sorts of techniques used to implement JSON support in modern languages. Or sometimes it'll just be the dominant library for dealing with it just has an old design that baked bad assumptions in, and since it's the dominant library it's the one everything uses, so I have to deal with that everywhere.

And it's just the death of a thousand of those cuts. "But you can do JSON in my favored language!" Yeah, but it's just not quite as slick. "But we have an HTTP client in this language!" Yeah, but it's just not quite as slick. "But we have GPU support in my favorite language!" Yeah, but it's just not quite as slick. And you've ground all that "not quite as slick" deeply into your language over the decades.

So nobody has any one reason they can point at as to why Ada isn't going come back, or why E isn't going to come back, or why Cyclone isn't going to come back... but the reality is that the sum total of the issues is more than sufficient to prevent it from ever happening, and what's going to happen is a more modern language is going to get the support.

Advocates also try to "defeat in detail", in analogy to the military technique, arguments to the contrary, but the problem is that while that may satisfy the advocate, everyone else is still left looking at a metaphorical battlefield that has an exhausting number of "battles" over basic deficiencies, and being "defeated in detail" by an advocate just transfers to exhaustion with the underlying language anyhow.

It probably isn't a "the issue" with Ada/SPARK. It's a horde of small little things, the sum total of which is too much hassle for anyone to want to deal with.

Why are you using past tense for Ada? Adacore is still doing business and Ada 202x will be standardized this year or next.

I’m also not sure why “nice JSON libraries” is a hard requirement for kernel code. Also, see JWX.

Why past tense? Because it's dead as languages go. Defining "death" as "zero users" is not the definition most people use, because it's not useful; things are clearly dead before that point. Ada doesn't have a bright future. It isn't going to rise from the ashes and have everyone agree that yes, it was right all along, and everybody with 10 years of experience on their resume is suddenly in hot demand as the crowds give them ticker tape parades for having been right all along. That never happens. It may well klunk along for more decades... but it's dead.

What does happen with such languages is that someone comes along and creates some sort of new language taking the best of the old language and mixing it with more modern stuff. I personally think there's an Ada-like niche waiting to be exploited there, probably something that also takes some lessons from Haskell. (Haskell is still alive, but IMHO, headed toward this sort of dead right now, and really could use this sort of revival itself.) An example of this is Elixir... Erlang would probably be also something I'd be calling "dead" if it weren't for Elixir.

(Ironically, often the biggest partisans of the base language are the last to know about the revival language because every deviation from the base language is seen as a flaw from the One True Answer....)

Ada should be considered dead because it doesn't have an npm full of super[1] useful[2] libraries?

> That never happens. It may well klunk along for more decades... but it's dead

Ada is used in 2021 in the exact same places that Ada was used in 2011 (and 2001 before it), if not more. Ada was designed for a specific purpose, one that it still fulfills very well. People have been claiming Ada was dead for decades, yet still it miraculously lives on. Despite Rust, despite Haskell, despite an algal bloom of "formally verifiable subsets of C", and so on.

> What does happen with such languages is that someone comes along and...

Yet... This just... hasn't happened. A successor language more suitable for safety-critical development has just simply not appeared. The manufacturers using Ada —a subset of which can be seen at this[3] link— ostensibly don't seem convinced that any of Ada's many alternatives offer a more appropriate solution for developing safety-critical software.

> I personally think there's an Ada-like niche waiting to be exploited...

The Ada-like niche you describe is, believe it or not, currently occupied by Ada. Ridiculous as this may sound, Ada is actually pretty good at fulfilling its intended function. What needs to change? Ada is not designed to fill the role of Node.js, Java, or C#. It's designed for safety-critical embedded systems, which is where you're most likely to find it today.

> Ironically, often the biggest partisans of the base language are the last to know about the revival language because every deviation from the base language is seen as a flaw from the One True Answer...

Does this apply to your thinking too, or just the proponents of Ada, and other languages you don't like? Are the Rust users just blind to the benefits of Ada? Are you susceptible to the same cognitive blind-spot you accuse us of having?

[1] https://www.npmjs.com/package/pad-left

[2] https://www.npmjs.com/package/is-array

[3] https://www.adacore.com/company/our-customers

> Ada should be considered dead because it doesn't have an npm full of super[1] useful[2] libraries?

Wait! There is Alire[1][2]! There is a list of "crates", you can easily include them into your project, and so forth. This is pretty much the same as https://crates.io or https://pkg.go.dev, which means people really should throw their misconceptions away and actually do some research before concluding that the language (Ada) is dead. A couple of quick searches quickly tells me that Ada is pretty much alive, with all of these "modern libraries with modern solutions", and full-on safety without performance loss.

This comment is intended for the person you replied to. :)

[1] https://alire.ada.dev/

[2] https://blog.adacore.com/first-beta-release-of-alire-the-pac...

So dead "because I said so" in essence?

Very few users over a long period of time means very few are working to keep the language up to date.

Too long of this pattern and it becomes much more trouble than it's worth to use on a business level.

Having 7 compiler vendors, happily in business, from people that actually pay for compilers, and an upcoming language revision, seems healthy enough.

No more than you're saying it's not dead "because I said so".

They gave a bunch of reasons.

Yeah. "Not just quite as slick". What does it even mean? Ada/SPARK has everything you would find in a modern language... and more. People hold lots of misconceptions over the language, that is why I often bring it up and talk about it. That is why I often provide links to stuff people would easily find if they were to look stuff up about the language. As I said in my other comment, it even has a package manager: https://alire.ada.dev/.

Now, I know that there is a trendy view of "the more the better", and it does not have as many libraries there, but that has to do with the fact that it is not yet widespread among Ada users. Alire is really new.

Not sure what you mean about Haskell. Haskell is seeing more activity than it has even seen!

What kind of scalable approach are you describing? Rust is not formally verifiable. I'm aware that there are projects attempting to solve this problem, however as I understand it you can't currently create verifiable production code.

> focusing purely on type- and memory-safety, not conformance to arbitrary specifications

What are types if not arbitrary specifications? Are you suggesting that formally verified software is not memory safe? What on earth does "scalable" even mean? A verified program cannot scale? If not, why not?

Types are not 'arbitrary' in any real sense. Type systems can be described as a sort of formal verification that leverages and is closely aligned with the syntax structure of actual code, thus type systems can preserve compositionality but don't generally support non-local reasoning, at least not in a very elegant way. This is exactly what can make them potentially more scalable than other sorts of FV, hence more useful for programming "in the large".

Types that can be defined by users are, necessarily, part of a language syntax, so that they are aligned with the syntax is just a tautology. Equating user defined types with formal verification is just nonsense. C has types. Python has types. Rust has types. That the program does what you think it should do does not logically follow the mere existence of types. I have no idea what "in the large" is supposed to mean. I feel like GPT-3 is arguing with me.

Maybe I can try to explain the parent comment's point a different way. When saying that rust works on types and not on arbitrary specifications, I think he is saying that rust is more limited than languages that support arbitrary specifications. However, by making this tradeoff it achieves a reasonable degree of safety without incurring a ton of overhead.

I believe the comment that types are aligned with the syntax is meant as a contrast to other languages which include specifications written in a format substantially different from or fully removed from the implementation. This can reduce the friction of using type-based verification when compared to formal verification capable of describing an arbitrarily complicated spec.

When discussing the scalability of types, I think he is saying that because types are coupled to the implementation, and don't support non-local reasoning, it is less likely that you will run into issues with type checking as you try to compose many small components into a larger program. In contrast, my impression is that with full formal verification, it can become extremely difficult to properly verify a large system.

Regarding your comparison to C and python, I think it's clear that the parent was comparing the specific type system and borrow checker that Rust provides vs. formal verification, not making a statement about the general concept of a type system. In particular, I don't think it's reasonable to assume he was saying the existence of types provides any sort of safety. Rather, it's clear he was saying the use of a powerful type system (such as that found in Rust or Haskell) to implement a limited specification of the program functionality can provide a degree of safety.


"In other words, the Curry–Howard correspondence is the observation that two families of seemingly unrelated formalisms—namely, the proof systems on one hand, and the models of computation on the other—are in fact the same kind of mathematical objects.

If one abstracts on the peculiarities of either formalism, the following generalization arises: a proof is a program, and the formula it proves is the type for the program."

I believe what zozbot234 is saying is that Rust focuses on a specific subset of formal verification, and on trying to make a language with that enforces that subset in a way that is still somewhat ergonomic.

I'm assuming "scalable" in this case is referring to the fact that fully verifying a piece of software is currently takes a large amount of effort. Rust's approach is more "scalable" in the sense that they decided to focus primarily on memory safety, and punted on other forms of verification in the hope that it would be more ergonomic/require less effort.

> I've never read anything to make me think that Rust is a safer alternative than any of these options; the guarantees of the language are just assurances of its advocates.

Note that some formal verification work has been done on the guarantees that the borrow checked provides (which led to finding and fixing an edge case bug), so there is a little more concrete evidence that just the "assurances of its advocates"

See http://plv.mpi-sws.org/rustbelt/ for more information, also the verification working group: https://rust-lang-nursery.github.io/wg-verification/

I don't think that the mere existence of a "working group" or grant funded research positions for verifying rustc or a subset thereof is the same as having a verified compiler. That's certainly not a strong argument to against using rustc for safety over one of the many verified compilers that actually exist. At least, I didn't see in the "rustbelt" list of papers anything which appeared to indicate that a verified compiler or language subset do in fact exist. Furthermore, that the proposed patches rely on the nightly compiler and a special variant of rust's core, which can only be enforced by special feature tags seems to suggest that Rust-Linux is not being written in this hypothetical, future compiler.

> At least, I didn't see in the "rustbelt" list of papers anything which appeared to indicate that a verified compiler or language subset do in fact exist.

You might want to look harder, because there is certainly a verified language subset (anything that can be written as LambdaRust, which covers a large and substantial swathe of the language).

If you're looking for a formally verified, optimizing compiler for any realistic language, particularly a low level language, you have pretty much one option: CompCert (I'm not sure where this large group of verified compilers you claim exists lives, but I'd love to see them). As someone who would love a verified Rust toolchain, I can't help but notice that very few safety-critical systems actually use CompCert in practice, which makes me a bit suspicious of claims that this is something Rust needs to be competitive in this arena.

Finally, I'll point out that verified compilers like CompCert only promise to translate correct C to correct machine code; they do not necessarily aid you in coming up with correct C in the first place. Miscompilations certainly happen, but not nearly as often as undefined behavior in the source program. So asking why people would use Rust when verified compilers exist for other languages is sort of missing the point.

I think Compcert isn’t widely used because of its license. GNAT is also GPL. Everyone lost their mind over Oracle charging a nominal sum for their compiler. I don’t think rust would have its corporate backing if it had similar licensing.

Also, there is only undefined behavior in rust. The compilers behavior can change at any time for any reason any time somebody with commit rights thinks that it should. You cannot begin to assert provenance about some thing that can change at any time.

> I think Compcert isn’t widely used because of its license.

I somewhat doubt this, but even if it is true, the fact remains that people are not actually using it for the vast majority of mission-critical software. This suggests that the elimination of miscompilation bugs, which is what you get from formal verification of a compiler, is not high on their list of priorities.

> Also, there is only undefined behavior in rust. The compilers behavior can change at any time for any reason any time somebody with commit rights thinks that it should.

This is certainly not true of Rust in any practical sense.

I am not saying Rust doesn't need a certified version of its compiler that people can legally rely on for stuff like this (as opposed to practically). I am saying that this objection has nothing to do with the existence of a formally verified compiler, which is also not in practice used to compile mission-critical C programs. I think you are confusing certification of a compiler for mission-critical software, with formal verification of the language's compiler, semantics (including type safety of the safe subset--a proof that would not go through for C as it explicitly unsafe), and standard library.

It has not been done yet, it is a work in progress, but it is being done. https://ferrous-systems.com/blog/sealed-rust-the-pitch/

My point is that solicitations for grant money do not provide the assurance that products that actually exist do.

Sure, I am here to state the current state of the world and point to the most up-to-date way to find out what the status is, that's it.

So... it hasn't been done

That is what I said, yes.

(Though, as pointed out by a sibling, there is a subset that is.)

Static code analysis is not enough for C: https://t.co/Pbo4iHqEub

Apologies. I thought I pasted the original link but I was wrong. Thanks for fixing it.

Formal verification techniques don’t scale, not even to your average CRUD app, let alone to an OS-scale.

In a number of ways I'd argue that FV of an average CRUD app is a very hard problem, for two reasons:

- the requirements generally change quite frequently

- the requirements are generally a long way from being "formally verifiable"

Where I, personally, have found the most value so far using FV techniques is from modelling "tricky" things whose requirements are quite solid. A few examples from my work:

- A state machine for managing LoRa communication. The requirements in the LoRa spec are pretty good. I took those requirements and designed a state machine I could implement on a low-power device and modelled that SM in TLA+ to verify that there were no deadlocks/attempted transitions to invalid states.

- A state machine for managing the Bluetooth communication between an Android app, a Bluetooth-Iridium (satellite) bridge, and the server on the other side of the Iridium link. Similar to the LoRa case, I used TLA+ to ensure that there were no deadlocks in my proposed SM (and uhh made a number of corrections as I went). Ultimately, due to the design of the BT/Iridium gateway, the exercise resulted in the conclusion that it wasn't actually possible for this process to be 100% reliable but it was possible to detect and retry the edge cases.

- Modelling a somewhat awkward email/SMS invite flow for a mobile app. You could get an invitation over email or SMS, and your account transitioned through a few different states as both your email address and your phone number were verified. Modelling this helped ensure that your account couldn't get into a state where no forward progress was possible or into a state where you could use a half-completed account.

Thanks for the informative answer!

Just a note, I (personally) don’t consider TLA+ a FV technique — it is a really good technique that actually scales much better than formal verification programs like Agda or Coq.

It's formal verification of an abstract machine as opposed to running code. The problem is that formal methods as a field doesn't yet have a rich enough vocabulary to distinguish between its flavors. I use "code verification" and "design verification", which is a little more specific, but has its own issues.

Is TLA+ a sandwich?

> TLA+ is a formal specification language developed to design, model, document, and verify concurrent systems.

But it only proves a model, not the actual code — that’s a major distinction.

You can't write a bug and nor can you write a test if you don't even have proper spec. But it happens a lot when requirements are just ambiguous.


Let us see what they have, using formal verification (Ada/SPARK).

- JWX is a library for handling JSON data and more. It is implemented in the SPARK programming language and has been proven to contain no runtime errors. As a result, JWX is particularly suited for processing untrusted information.

- The RecordFlux specification language is a domain-specific language to formally specify message formats of existing real-world binary protocols. Its syntax is inspired by Ada. A detailed description of the language elements can be found in the Language Reference.

- Formally verified, bounded-stack XML library

This is just Componolit.

Let us check the F* language:

- F* (pronounced F star) is a general-purpose functional programming language with effects aimed at program verification. It puts together the automation of an SMT-backed deductive verification tool with the expressive power of a proof assistant based on dependent types. After verification, F* programs can be extracted to efficient OCaml, F#, C, WASM, or ASM code. This enables verifying the functional correctness and security of realistic applications. The main ongoing use case of F* is building a verified, drop-in replacement for the whole HTTPS stack in Project Everest. This includes verified implementations of TLS 1.2 and 1.3 and of the underlying cryptographic primitives.


Given the above, what exactly do you mean that it does not scale?

Whoops, I completely forgot about libsparkcrypto (https://github.com/Componolit/libsparkcrypto) which is a "formally verified implementation of several widely used cryptographic algorithms using the SPARK 2014 programming language and toolset. For the complete library proofs of the absence of run-time errors like type range violations, division by zero and numerical overflows are available. Some of its subprograms include proofs of partial correctness.".


* AES-128, AES-192, AES-256

* AES-CBC (all supported AES modes)

* SHA-1


* SHA-256, SHA-384, SHA-512

* HMAC-SHA-256, HMAC-SHA-384, HMAC-SHA-512


* RIPEMD-160



It is pretty awesome. :)

Looking at the examples you've provided, I'm pretty sure the Linux kernel's codebase dwarfs their combined codebases into insignificance. Since it is very hard to not have NP-hard asymptotic complexity when formally verifying a codebase as large and as demanding (in terms of performance, etc) as the Linux kernel, I would expect that if you tried to rewrite Linux in the languages you've mentioned and formally verify the rewrite, you will be able to keep the entire AWS cloud (globally) very busy for a very, very long time. On the other hand, if you were to do the rewrite in Rust and use some hypothetical formally verified Rust compiler to type check it (which is mathematically equivalent to such a formal verification in, say, F* limited to only verifying certain properties), it'll probably type check in minutes or even seconds on the laptop I'm currently writing this reply on.

For a less hypothetical example. RedoxOS has a codebase that dwarfs Sel4 (but it is still much smaller than Linux in turn), yet it type checks with much less compute cost than it takes to formally verify Sel4. Or heck, Redleaf actually formally verifies in a tiny fraction of the time it takes to formally verify Sel4, because the Rust type checker not only significantly reduces the amount of requirements that still needs to be formally verified but also reduces the complexity to verify those requirements to linear to the codebase size due to the restrictions that the Rust type system and module system puts on valid Rust programs (with a little bit of care when writing the code). Of course, until you have a certified Rust compiler there might still be miscompiles of Redleaf and until all the features of Rust used in the Linux kernel is formally specified, we cannot do the same with the Linux kernel as for Redleaf even if somehow all of Linux got rewritten in Rust. But in Rust at least it is conceivably possible given sufficient resources and sufficient time. I very much doubt it will ever be possible without help from a sufficiently expressive and practical type system.

Oh yea. Then there's another problem. Most (all?) of the examples you've mentioned have requirements that are well specified and pretty much set in stone. The requirements fro the Linux kernel... aren't quite as obliging.

Sel4 is an OS that is formally verified.

It's security parameters are well-defined enough that you can use it to launch isolated VMs with... less secure OSes that are sandboxed from each other.

I was under the impression that SeL4 exists.

That's true, but as a microkernel, seL4 has a very limited scope. It's not in the same ballpark as, say, the Linux kernel. It's more like a hypervisor. [0]

From a quick google, seL4 has around 10,000 lines of C code, whereas the Linux kernel has around 30,000,000.

[0] https://sel4.systems/About/seL4-whitepaper.pdf

Kinda. https://news.ycombinator.com/item?id=27232401

I think CSIRO disbanding the team was a huge mistake, but in any case they weren't producing the kind of success metrics that sustained their funding.

I know of at least one other company that is picking it up.

Testing is hard. And (very) expensive.

Formal verification is even harder. And even more (very) expensive.

ROTFL. Microsoft is interested in security ? Maybe they shall start with their own OS. (Solar Winds, Wannacry, ransomware)

'except' Who? ARM?

Well [0]

[0] https://github.com/ARMmbed/mbed-os

Also to note, ARM toyed with the idea of using a Linux distribution as alternative to MBed, but it was short love, it is already dead, it only lasted one release.


Very true. Fuchsia was also initially prototyped with a Linux kernel and well, the rest was 'history'.

Note that MBed Linux was created after MBed already existed, they just toyed with the idea of offering MBed userspace on top of Linux.

Linux isn't an OS and every one of them relies on it for mission-critical infrastructure.

Isn't it a little bit early?

I have distinct feeling this would benefit from waiting a little bit more to have various kinks straightened out.

The kinks get straightened out by people working with it and trying to make things. Waiting won't accomplish that.

> Like it was mentioned in the RFC, the Rust support is still to be considered experimental. However, as noted back in April, support is good enough that kernel developers can start working on the Rust abstractions for subsystems and write drivers and other modules.

I also believe that this is a little bit hype driven but not quite. I've been talking with a Linux dev at a conference in Cluj and he said that people nowadays are not interested in Linux development as he was in high-school because there's so much more out there and way easier to enter (web, mobile, game dev etc.). A new language like Rust can reinvigorate the Linux ecosystem + the benefits of safety and other language features. Zig could have been an alternative but unfortunately it's still under development and quite far from a 1.0. But, in my opinion, once you fragment the ecosystem with Rust, adding a third language like Zig should not be a problem. So, yeah, the train still hasn't left the station.

Honestly, I think this particular argument is bogus.

From my point of view what counts is actual kernel development. If you are going to develop kernel because it uses cool new language but you would not if it was still C, you are probably not the right person.

Now, I think Rust has potential to be good kernel language, I am mostly concerned with toolchain, ability for people to read the code with comprehension, ensure correct code, etc.

> If you are going to develop kernel because it uses cool new language but you would not if it was still C, you are probably not the right person.

You are taking this the wrong way around. It's not about people contributing to $PROJECT because it uses $COOL_TECH, it's about people being turned off from contributing to $PROJECT because of $MEH_TECH.

If Linux was written entirely in assembly, we'd be having the same argument about the introduction of C.

Ironically UNIX was indeed written in Assembly, and C only came into the picture with V4.

Also BCPL, the basis for B intepreter, was originally designed to Bootstrap CPL, not really as a daily use language.

As a potential alternative thought process I would add that kernel development sort of uses their own flavor of C that you also have to learn. While in case of a language with better abstraction powers, you can actually read a function and knowing only the language but not the project, could potentially contribute — as opposed to C, where I have to know this cryptic macro, and that by convention this and that struct has to be embedded x bytes into another struct so that it can be used with the linked list utilities made.

Also, simply by having god damn namespaces more readable names could be used at no downside.

> From my point of view what counts is actual kernel development. If you are going to develop kernel because it uses cool new language but you would not if it was still C, you are probably not the right person.

Why's that? C is a tedious language that makes you do so much manual bookkeeping, I don't think I'd ever write it again (if I needed C for some reason I'd write a program to generate it for me rather than doing it myself). I think any decent developer would be put off by C to some extent. Sure, the people who really want to make a kernel may put up with it, but an arbitrary enthusiasm barrier is not the way to attract good contributors.

> I think any decent developer would be put off by C to some extent.

Any decent developer would be put off by any language to some extent.

Personally, I'm more put off by Rust than C (they put me off for different reasons). Currently, the one puts me off the least is Zig, but it still has many details that I don't like.

On the other hand C is simple language, there are no discussions about how to do something in C between people who know C.

C is tedious but kernel programming isn't about spewing vast amount of code anyway. It is more important to be able to read it, understand it and ascertain it is correct. This is one of main reasons for why C++ is not there.

> C is simple language

Except for, you know, all that Undefined Behavior stuff, which makes it practically impossible to write correct programs even for very skilled developers, or the lack of abstractions, which makes it hard to safely re-use advanced data structures.

"C is a simplistic language" would be more accurate.

C encourages simplicity.

Code is either clear and simple, or extremely obscure and safe, or kinda in between is complicated but not complicated enough such that its not safe.

"Simplicate and add lightness" aerospace mentality people like C.

At some point any project expected to do ever more complicated tasks, like a kernel, will be unable to use simple C and will have to take the hit of a more complicated language.

Simple is good when matched to simple tasks; my microwave oven or TV should ideally never data network with the external world and never malloc memory and never do string processing. C makes an amazing toaster or car automatic transmission controller.

C is simple only as a pseudocode language, i.e. to reason about the happy flow. As soon as you start adding corner cases and error handling, all your happy flow code now gets obscured by numerous ifs, switches, and ($deity forbid) goto statements. Then, add pointers masquerading as output parameters, pointers masquerading as arrays, and pointers masquerading as pointers and your language isn't so simple anymore.

Flintlock pistols are simple, do you think they are more reliable or easier to use than an AK-47?

Which one would you rather defend yourself with?

C++ is definitly there, just not on Linux.

>"I think any decent developer would be put off by C to some extent."

Call me indecent. I use C for firmware development running on small microcontrollers and consider it perfect for this particular task. Not put off by C for this task at all.

It is a little bit bogus, I did not say that I stand by it or that I think that this is the WAY. I'm not even a Linux developer or a kernel dev, though I've done embedded programming at the beginning of my career. Just that if we won't take risks, we will never know whether the approach of Rust or Zig or just plain-old C would prove to be THE approach to systems programming. Besides fragmentation, how else can you harm what we already have? I believe the ecosystems fix themselves, if you offer to the developer three choices (in our case C, Zig, Rust), we will see how things pan out and we will have a clearer picture. Java did not become the language of Fortune 500 companies out of sheer luck, people simply chose it more often than its counterparts because the feedback was positive. I expect the same in systems programming.

a couple of things:

1. rust is easier to read than c/c++

2. The toolchain is llvm based and much nicer to use than c/c++. Hell your build scripts are also rust

3. Given the choice to develop in c or rust I would choose rust

4. In my own experience I have found rust to be simpler to Deal with correctness than c/c++

(I have been both a rust and c++ developer)

> 1. rust is easier to read than c/c++

Rust may or may not be easier to read than C++, depends on your experience.

But it is not true it is easier to read than C. C is objectively much smaller, simpler language than Rust.

> 4. In my own experience I have found rust to be simpler to Deal with correctness than c/c++

That is the whole point of Rust. And also to do this with minimum runtime overhead.

C is a smaller language on some axes. That's not necessarily a good thing.

Looking at the following function definition, can you figure out how to use it safely?

    int foo(char* text, char* out,
            char* s, char* x);
If you were to have the same signature in Rust, it would look more like the following:

    fn foo(
        text: String,
        out &mut String,
        s: &str,
        x: &mut str,
    ) -> i32;
Now it is clearer that foo is responsible for getting rid of the allocation corresponding to text, which is on the heap. out can be modified and potentially reallocated. s is read only and it won't be deallocated by foo. x might be mutated in-place by foo, but it won't be deallocated.

Having a more "complex" way to represent in the typesystem something that C only bothers to call "a pointer" makes things better: safer, easier to skim, explore and understand an API, and allows the compiler to catch API misuses.

Being a smaller simpler language doesn't make it easier to read or write. Go is an even "simpler" language than C, but you quickly suffer from boilerplate-blindness when reviewing it. Being able to write good abstractions can make a huge difference. Having lifetimes, or the use of the semantically-correct integer type checked by the compiler reduces the cognitive load on the writer and reviewer.

>"is objectively much smaller, simpler language than Rust."

Brainfuck is an even smaller, simpler language, it has only 4 characters!

Yep that is my experience. C++ sucks. Thinking in rust and getting your ideas out is much much much easier. C is portable assembly, I prefer a language that protects me from footguns. I have better things to think about.

It's even worse, C is “portable” PDP-11 assembly. It has been a few decades that a C program is only distantly related to the assembly the compiler will generate.

On the Rust vs C++ scenario, try the next level with Rust:

- GUI code

- Generic datastructures crates coupled with lifetimes, macros and attributes

The way I'm reading it, that's exactly what's happening here

In what way? Rust seems to be proving itself as a reliable mainstay in systems development


The git repo has over 150,000 commits, 3,000 contributors, and 9 years of release history. The last 6 years of which have been post 1.0.

Also, Mozilla has been writing large parts of firefox in Rust since ~2017. There's some interesting writeups on hacks.mozilla, including this one on reducing CVEs with Rust

https://hacks.mozilla.org/2019/02/rewriting-a-browser-compon... https://research.mozilla.org/rust/

Sizes of repos have nothing to do with it. By that measure we should all leave C and convert kernel to C++.

I do embedded development on ARM Cortex-M3 and while it is possible to do this in Rust, I have experienced a bunch of issues with the toolchain and I have decided to stay on C until toolchain improves.

Don't get me wrong, I like Rust. Just don't allow liking something get in the way of practicality.

> By that measure we should all leave C and convert kernel to C++.

Microsoft actually did do that in the 90's.

No. Most of the kernel is in C. Some parts have been in very light c++ since the 2000s.

Vista changed that, as Visual C++ gained stable kernel support, it has been a couple of years now.

Anyone feel like we get a "Linux Rust support" post every month lately?

Feels a bit like the "new more efficient battery technology" recurring post.

edit: to precise it's not that I'm not supportive of the effort, just that it would be nice to just have a post when it's actually merged. The title is a bit deceptive

I quite appreciate the reports. I normally don't follow the linux kernel development, but the possible support of Rust is one major step for the kernel which is hugely interesting.

The Linux kernel has become one of the most, if not the most important piece of IT infrastructure. Progress of any further developments of it as well as the security itself are prime concerns for all users. So far the development was solely limited to C, with all the tradeoffs. It is highly interesting to see whether a more modern language can be incorporated and the Rust effort looks very promising. Both from the language capabilities as well as the progress being made.

That's because the "merge window" is open once every ~2 months; this is the second time this series is being sent, with improvements based on feedback from v1.

If enough people find it interesting enough to follow, why not?

Any UNIX clone that decides to have other languages alongside C on their internals is welcomed news,

Ada, C++, Java, Objective-C, Swift and yes Rust.

Are there any interesting OSs in the others? I know about redox, but I haven't heard of anything outside of C and rust.

Serenity (C++)

Well, Slackware has all of them :p.

Ok. So... Will I need to have two compilers to build the kernel? gcc and rustc(LLVM)?

You'll also need make, bash, perl, and more... [https://www.kernel.org/doc/html/v4.15/process/changes.html]

Also, rust is only being considered for kernel modules, not kernel core. And even then, only kernel modules that don't need to build on architectures rust doesn't support. So if you don't need any of those particular modules you can just disable them.

In the long term, LLVM/Rust support for more architectures improves, and support for older architectures is dropped, this will become a larger fraction of kernel modules, but it will be a very long time until it is considered for something like ext5.

The email also gives an update on ongoing work to add rust support to GCC.

Not familiar with C compiling besides a few small programs I wrote back in college but can Linux not be compiled currently with LLVM?

Linux can be compiled with LLVM (clang), and the current rust code strongly prefers that you do so. It's possible to do gcc + rustc, but it's less supported, and if you pass the wrong gcc flags I believe it just won't work.

It can, but up until just a couple of years ago it could not as it used a lot of GCC specific syntax

> until just a couple of years ago it could not as it used a lot of GCC specific syntax

Note that the kernel still uses a lot of GCC specific syntax; it's just that LLVM/clang was laboriously made to understand all of that (with a few exceptions where the kernel was changed instead). And when they were almost done, the kernel started requiring another new GCC specific syntax, so they had to chase after that too.

It seems you can already write kernel modules in Ada: https://github.com/alkhimey/Ada_Kernel_Module_Framework. Obviously it comes with a boatload of restrictions [1], so no tasking, RAII, exception propagation, or dynamic allocations.

[1] https://github.com/alkhimey/Ada_Kernel_Module_Framework/blob...

You can already write kernel modules in Rust too.

The point is to integrate the Rust language to the Linux infrastructure so you can merge rust drivers to the official code base.

This might be a stupid question because I don't know much about Linux development. Have these patches been accepted into the kernel? Or are they still just "propsals"?

Still just proposals.

They've been accepted into linux-next, which is a staging ground and used for testing, but that by no means guarantees that they will ever be accepted into the mainline kernel.


Not going to be merged into a release branch yet, this is more of a "status update, give it a try" posting. We'll certainly see a few more of those before we get a proper Rust-enabled Linux release.

I don't fully understand it either, but they seem to be merged into linux-next, whatever that exactly means.

Wow, I'm impressed that alloc crate modifications are already there ! Seeing this rate of progress (and the funding behind this work) makes me quite optimistic !

Beginning of the end of Linux I guess... Mixing multiple languages deeply in the core rarely works due to different requirements and limited interoperability. 5 years later we are going to read about how to migrate existing Rust code to C, like what's happening to Scala projects these days.

It seems to me like a Trojan horse from G and MS that pursue their own interests with their own OSes.

> like what's happening to Scala projects these days.

I don't know much about Rust so can't comment on that part. But agreed on the Scala part. Having seen Apache Kafka use Scala in the early days, when Scala was considered "hip", alongside Java code in the same codebase, I can relate to the mess it created and continues to be even today. At some point there was a plan to move away from Scala in Kafka, not sure where that reached, I stopped following that project since a few years now.

But another jvm language (kotlin) seems mixed with java just fine.(did it designed to do so?) Two way calls just work as is. Interfaces just maps to interface in each other. The only problem is probably the gradle config, but it is a one time thing.

> 5 years later we are going to read about how to migrate existing Rust code to C, like what's happening to Scala projects these days.

Just the opposite. We're going to see C deprecated for new code and efforts to move the existing C codebase to Rust. C is pretty much unsafe at any speed; Rust allows even junior front end developers to fearlessly contribute bare-metal code once they've learned the language.

Ah, but Rust will help reduce security problems! Even if the number of potential Linux contributors is cut to a fraction due to the difficulty in learning two languages with steep learning curves, better security makes it all worth it.

The Linux developer pool will increase. C programmers are mostly old hands these days, and they're a dying breed. Rust opens the possibility of kernel development to younger or less experienced programmers, many of whom only have had experience with modern languages and frameworks.

I program in C and I'm in my early 20s now and still create new projects or write C on a regular basis.

This is false

Thanks for sharing the opinion. However could you elaborate why you think it's false?

...even worse.

If you can't see how having inexperienced programmers writing code that is guaranteed memory-safe beats having world-class expert programmers writing dangerous code because even world-class expert programmers cannot wield C safely then why are you working in the field?

Is this a joke? Is the existing infrastructure built by countless geniuses in C not working at all? Do you think inexperienced programmers could build it given a "safer instrument"? How many junior devs understand intricacies of basic OS-level locking, not mentioning Paxos and other scary algorithms whose formal correctness can't be even proven in theory?

> Is this a joke? Is the existing infrastructure built by countless geniuses in C not working at all?

Given all the CVEs that arise due to buffer overflows and UAF, it's not working very well. Safe Rust makes those classes of problems Just Go Away.

> Do you think inexperienced programmers could build it given a "safer instrument"?

Inexperienced programmers can get started without the near vertical learning curve C presents. Just wrapping your head around pointers scares many programmers off, and even once you grok pointers, attempting to use them correctly is a minefield. This makes kernel hacking daunting for the average dev. Rust gives them an onramp.

> How many junior devs understand intricacies of basic OS-level locking, not mentioning Paxos and other scary algorithms whose formal correctness can't be even proven in theory?

Not very many... but junior devs don't need to work on that stuff. They can make more peripheral contributions -- fixes to device or file system drivers, etc. -- while they're building their skills, completely confident that they will not make a class of stupid but very common and dangerous memory errors. Not so with C! As I said, not even great programmers can be relied upon to write safe C code -- the model presented by C is just that abstruse.

Scala actually reminds me a lot of Rust. It’s at about the same complexity level in my eyes.

Scala doesn't care about efficiency or cost of what it's doing, all the fun fancy features allocate like crazy.

Not in my experience. To me, Scala feels like a kitchen sink language - like C++.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact