(Safe) Rust is Data Race Free. You can mistakenly write a data race in Go, just as you could in C, and, even though under normal circumstances Go feels like it's memory safe, once you've got a data race all bets are off and you potentially no longer have memory safety. In (safe) Rust you can't write a data race, so, this can't happen.
If you write simple serial programs, you don't care, your programs never have data races because they have no concurrency and therefore can't possibly have concurrent memory writes. But obviously Linux is not a serial program.
We proven time and time again we can't write safe c/c++ code from a security perspective. I don't think we've proven that crashing now and then to fix our data races is a bad outcome. There are always bugs to be fixed.
The big problem is SC/DRF. Most languages promise (at best) your program is sequentially consistent if data race free. And it turns out we can't debug non-trivial programs unless they're sequentially consistent because it hurts our brains too much.
Causality is something we're all used to in the real world. The man hits the ball with the bat, then the ball's trajectory changes, because it struck the bat. Sequentially consistent programs are the same. X was five, then we doubled it, now it's ten.
But without sequential consistency that's not how your program works at all. The ball goes flying off over the wall around the field, then the pitcher throws the ball, the ball lands in the catcher's glove, the umpire calls it, the batter hits the ball, and yet at the same time misses the ball... We doubled X, now it's five, but before we doubled it that was nine or sixteen? What?
It must be noted, though, that data races can lead to memory safety issues in languages which are otherwise free of them, Go being a prime example of that: the built-in hashmap is not thread-safe, and does exhibit memory corruption issues under unprotected concurrent writes and accesses (only concurrent unprotected reads are OK).
There is a “best effort detection” of concurrent misuse, but it’s just that.
C-style syntax and community interest also favor Rust.
This spec argument has always seemed like a red-herring to me. Can you explain why the Ada spec would be a significant factor in this instance?
I think GC is optional with Ada, as far as I know the memory safety comes from raising exceptions (or refusing to compile) when it detects memory-unsafe operations (array bounds checking etc).
>C-style syntax and community interest also favor Rust.
That's fair, C-like languages are instantly familiar with software people and rust seems to have a more hip image than old man fuddy-duddy Ada.
>This spec argument has always seemed like a red-herring to me. Can you explain why the Ada spec would be a significant factor in this instance?
I'm not arguing for Ada over Rust (I'm not a software guy) so I don't mean it as a red herring, but wouldn't a suite of static verification tools and a formally verified compiler require a spec to be tested against?
I think a spec is often a red herring because a bunch of folks living in the slum of C, when asked if they would all like to move into Rust's nice 3 bedroom by the park, instead always seem to ask: Wouldn't it be better to form a committee about building us a cathedral? Ada might be better. Someone should try it, but until then I'll take Rust.
Remain interested in the potential advantages of Ada compared to Rust for Linux kernel development, if you would care to point me in the right direction.
there was also a lot of unchecked conversion under the hood.
(disclaimer: I haven't really paid attention to newer versions of Ada)
Ada is safe compared to the other languages of its day, but I'm not sure it compares favorably with Rust. IIRC it does have more of a focus on safe arithmetic rather than memory safety.
Ada shines in its specification power, how developers can express what the code is supposed to do (strong typing, ranges, contracts, invariants, generics, etc.). And then you can either check your code at "compile time" with SPARK [1], that provides a mathematical proof that you code follows the specification. SPARK also proves that you don't have buffer overflows or division by zero for instance. Or you can have checks inserted in the run-time code which greatly improves the benefits of testing as every deviation from specifications will be detected, not only the ones you decided to check in your tests.
In terms of memory safety, Ada always had an edge on C/C++ because of the lower usage of pointers (see parameter modes [2]) and the emphasis on stack allocation. Now with the introduction of ownership in SPARK it's getting on par with Rust on that topic.
[1] https://learn.adacore.com/courses/intro-to-spark/chapters/05... [2] https://learn.adacore.com/courses/intro-to-ada/chapters/subp...
Second, this is exactly the overconfidence that I find troubling. Vulnerabilities caused by memory unsafety are real, pervasive, and inevitable.
A few resources you should look at:
- the official reports/post by Mozilla and Microsoft about the percentage of vulnerabilities caused by memory unsafety
- the mailing lists with the Linux kernel issues (I don't imply any severity; just the amount)
There are many summarized posts for the lazier, and I'm talking about high profile authors (or authors writing on behalf of high profile companies). Here's a semi-random one:
https://msrc-blog.microsoft.com/2019/07/18/we-need-a-safer-s...
There's a crucial part missing: the investment [...] to build (memory) unsafe drivers.
I find it very troubling when memory unsafe language programmers don't weigh memory safety at all in their views.
(note that this doesn't necessarily refer to Rust; there's people who swear that one can build drivers also in Golang, so assuming that is realistic, the same reasoning applies)