I feel like one of the attractions to Ada for this sort of use case is its maturity, and "here's a proposal for a complicated feature, inspired by Rust, a language which young and rapidly evolving and in particular switched to a new borrow checker implementation less than two years ago and shipped it with known unsoundnesses and is working on a new borrow checker implementation as we speak" may not be attractive to Ada's usual users. :) (To be clear, I'm fine with the risk profile of Rust's borrow checker, but in part that's because I'm fine with the risk profile of using the latest stable Rust and picking up any fixes every six weeks. I'm fine with a more powerful feature that lets me develop code quickly and I'm fine with upgrading my compiler every six weeks to pick up any bug fixes; I imagine that people writing airplane control software are probably going to prefer something less powerful that hasn't changed in decades.)
Honestly, I think one of the questions here is community. I don't really know who the Ada community is, beyond press releases from Adacore about planes and trains. I suspect that community simply does not care about safe dynamic allocation, even if it were available as a supported option, so they aren't going to be excited about testing out this feature. Is there a user community who would use this, in production (doesn't have to be a company, the "serious hobbyist" open source dev is fine and probably even preferable here), within the next five years or so? Are there folks writing stuff like high-performance grep replacements in Ada or hardened HTML 5 implementations in Ada?
I'd love to see (or help with!) such a comparison, but I get the sense that Ada's and Rust's use cases are so different that writing a fair apples-to-apples comparison is hard and even finding someone to do it would be hard.
> I imagine that people writing airplane control software are probably going to prefer something less powerful that hasn't changed in decades
True, depending on the design assurance level a certified compiler is required.
> I suspect that community simply does not care about safe dynamic allocation
See the reference in my former post. Whether and when the certification authorities accept it is yet another question.
> Is there a user community who would use this, in production ...
It's easy to find projects on Github where dynamic allocation is used; e.g. https://github.com/ghdl/ghdl; with the current developments, such applications may also have a chance for formal verification in the future. And no doubt it would help if the Rust compiler was formally verified as well.
As far as I know, the only usable formally-verified compiler (for a serious programming language) is the CompCert C compiler. Even C compilers and Ada compilers intended for use with critical systems, don't tend to be formally verified.
Of course, it would still be great if the compiler for Rust (or Ada, or any other language for that matter) could be formally verified.
It's unfortunate that CompCert isn't Free Software.
I think that's true for software developed under similar processes, but (for instance) if you're comparing software that has unit tests and software that doesn't, the constants are probably wildly different. Your tests (or even the process of thinking about writing testable code) will discover a number of errors but will hopefully drive the number of actual errors down.
To be clear, I'm not making a statement on whether Rust or Ada is better-tested or better-developed, but I will note that Rust goes out of its way
I'm also curious about these bugs - I'm aware of bugs in the standard library (which is developed in the same repo as the compiler), but they only undermine memory safety against hostile source code, and hostile source code has lots of other options (unsafe, /proc/self/mem, ptrace, ...), i.e., the Rust compiler is not a sandbox. I'm not aware of severe bugs in the compiler, and I'm not aware of standard library bugs against hostile user input by well-intentioned source code - e.g., there shouldn't be things like the 2001 sudo "vudo" exploit.
Of course, this is not a law of nature, but simply a reasonably plausible heuristic, which somewhat justifies my reluctance to a new technology, which was received with much enthusiasm.
CompCert is an extremely impressive achievement, and compiles a near-complete subset of standard C. A verified Rust compiler would be an enormous undertaking, and would need a very skilled team. It also wouldn't be worth trying unless the Rust language were very stable, which, if I understand correctly, it isn't.
Rust added a new borrow-checker implementation, "non-lexical lifetimes" (NLL) in December 2018, as part of introducing the 2018 "edition" (a compile-time flag that says what compatibility level you're targeting, roughly analogous to --std=c99). In 2019, they backported it to the original 2015 edition and removed the original implementation, "AST borrowck". As the names imply, NLL has the ability to handle more complex patterns without assuming borrows are live for the entire lexical scope just because it's accessed somewhere in a pair of braces; this turns out to be very useful in practice, since a lot of natural patterns (including those written by beginners not trying to do anything complicated) trip up the older implementation. However, NLL initially accepted some code that was invalid, and it was shipped anyway, and at least a couple of production Rust users ended up writing things incorrectly accepted by NLL. See https://lkml.org/lkml/2020/8/23/214 for my summary of what happened with some links. (I don't think this caused any problems in practice; my sense is that it was undefined behavior, which shouldn't be possible in safe Rust, but the compiler almost certainly chose a behavior that happened to match the intended semantics.) And there's work in progress on a new borrow-checker implementation called "Polonius."
All this is to say that, if you wrote a paper in 2018 saying that Rust's (AST-based) borrow-checker feature is great and Ada should pick it up, you're still behind Rust because there's a new one. If you wrote a paper in 2019 and based your work on NLL, you stood a nonzero chance of picking up that bug. If you write one today, maybe you should base your work on Polonius, but Polonius will itself probably take a fair bit of real-world use to shake out its own bugs.
> It's easy to find projects on Github where dynamic allocation is used; e.g. https://github.com/ghdl/ghdi
Thanks, that's useful!
Though (and maybe this is my unfamiliarity with Ada), from some quick looking around to see where it dynamically allocates, I find https://github.com/ghdl/ghdl/blob/master/src/synth/synth-hea... , which seems to bind the C malloc function and intentionally not bind free and leak all memory, am I reading that right? That's definitely safe but suboptimal.
Rust seems to be extremely focused on memory safety. Meanwhile Ada is much more focused on correctness in general. Restricting the discussion to simply memory safety ignores, well, most of anything that might be programmed.
Ada also has more memory safety options than people tend to talk about. As others have mentioned, it's possible to allocate quite a bit on the stack. Other rules also prevent some reference issues.
One thing I rarely see mentioned are memory pools and subpools. It is possible to ensure whole types are allocated in a particular subpool, and deallocation can be left for when the subpool falls out of scope.
- Nullable types (Option<T>), maybe-error results (Result<T. E>) etc. that force you to check whether you're looking at the right variant. You can't have bugs where you fail to check the error value and you use invalid/meaningless data, because you syntactically cannot express access to the data. This does often manifest as avoiding NULL pointer dereferences, which is technically a form of memory unsafety, but it's really preventing a logic bug. (For instance, this would have made the "goto fail" bug unnatural to write; that one was returning err = 0 as if it were an error, which you can't really do in the Result model.)
- More generally, sum types / tagged enums and the match and if let constructs, which enforce at compile time that you're accessing data from the right variant.
- Locked data that enforces that you hold the lock when you access the data, using similar means. You can enforce that there's no direct access to the data except through the lock wrapper, and more importantly, you can enforce that the lock stays locked as long as someone holds a direct reference to the data (i.e., that you can't leak a reference to that data and use it after you've released the lock).
- Safe threading/concurrency via labeling which types can be moved between or shared across threads. Again, this is technically a form of memory unsafety (data races) but it's more about logic.
- Typestate. You can avoid bugs where you use some logical resource when it's in the wrong state (read/write a closed file handle, send protocol data while you're still handshaking, etc.) if your API consumes ownership of the object in one state and returns the object in another state, and you don't have methods on objects of the wrong state. Rust pre-1.0 had typestate as a language-level feature, but it's straightforward to implement using the typesystem and the ownership model.
Really, I would say the core feature of Rust is a richer type system and the system of ownership and shared/mutable references. The most obvious thing to do with it is to prevent buffer overflows and use-after-frees, but it's not the only thing. (And that's also why I mentioned safe dynamic allocations, which rely heavily on the ownership system; without it, it's still pretty easy to prevent buffer overflows for static allocations.)
I don't have a sense of where Ada lines up on these. I know it has a much richer type system than C too, so it's possible it answers many of the goals besides safe dynamic allocations. I just personally see the benefit of Rust as more than just memory safety.
Off the cuff, I'd say Ada addresses all of those problems. In case you're interested, I'll leave a few terms that might be useful in delving further.
- Nullable types + sum types. Pointers can be declared "not null" which basically works as it says. Sum types exist as discriminated and variant records. Variants can be immutable or mutable, and obviously work to do the typical Option, Result, etc stuff.
- Locked data. Protected types do this. I imagine details might differ, but I know nothing about how Rust does this and haven't messed with them much or at all in Ada.
- Task types. I'm tempted to say more, but the little details matter so much for this kind of thing so I probably shouldn't. But Ada has tasking and concurrency mechanisms built-in to the language.
- Typestate. Compiler errors for this sort of thing are not immediately obvious to me. I can think of several options to try using even just the features I already mentioned, but I'm not sure what would or would not be detectable at compile-time. Catching incorrect usage and preventing it from causing trouble is more trivial, but just not the same.
The simplest and (in my opinion) most important feature in Ada is the ability to trivially create new types. So many languages require manually wrapping types. Better ones start to provide more magic to help automate it. But fundamentally none of them make user-defined types as a core component of the language. In Ada to create a new type it's just one simple line, and you automatically get full functionality of the base type while retaining incompatibility. The rest of the language and even the standard library is all designed around the idea of allowing the programmer to freely use these types.
You end up capturing so much more of the model that the program is using, and the compiler is able to check and ensure that the code is actually sensible according to that model. I find even the process of writing the types down helps expose flaws in the design I had in my head. Then once I start using it, it does a great job of catching when I start deviating from how I said everything should work.
Pretty much every other language I've ever looked at makes doing that sort of thing extremely painful. There is too much friction involved in detailing all of that, so nobody does. Then libraries are designed without it, which just increases the friction. Ada meanwhile makes it so easy to do that you feel bad not doing it, and you don't even gain much more than saving a handful of keypresses if you avoid it anyway.
The usual alternatives are to statically allocate all your memory, to convince yourself it's safe to use Unchecked_Deallocation, or to use a GC/refcounting library. Static allocation is usually not a problem for special-purpose embedded control applications: e.g., your airplane has two wings and one set of landing gear and its position is described by three coordinates, and you'll never need more of those. You probably want to avoid malloc anyway for both predictable performance and not having to worry about whether your allocation will succeed. But if you're writing, say, a CSS engine or a grep replacement or a terminal emulator, that approach won't work.
GC works for those use cases, but there are a number of excellent memory-safe GC'd languages already in wide use for many things, like Python and Java. You can get very good steady-state performance with Java, sometimes higher than equivalently-complex C, but it's still not a language you'd want to implement loadable libraries or OS kernels in.
Rust solves the problem of making writing high-performance, C-drop-in-replacement code feel much like (definitely not exactly like :) ) working in a higher-level language like Python or Java, including the memory-safety parts of that experience. Ada addresses memory safety, but for most of the use cases people are excited about Rust for, they want the combination of those features. For things like flight control software, picking something extremely mature (usually the companies in these press releases have existing Ada code from previous projects dating back decades) is valuable and having safe dynamic allocation isn't really a requirement.