> Nothing prevents you from writing Ada code that dereferences an access type after it's been freed; However any access dereference triggers a runtime check to ensure it's non-null. Unlike in C, freeing an access type in Ada automatically sets its value to null, and any subsequent attempt to dereference it will raise a Constraint_Error exception, which can be caught and handled.
> Ada has its own nomenclature for multithreading: Tasks, and provides its own built-in mechanism for preventing data races between them. Ada's Protected Objects encapsulate data inside an implicit mutex, allowing only one thread access at a time via a public interface.
I believe ADA doesn’t have a guarantee that you are accessing data thread safely. And that lack of guarantee is where use-after-free and double-free can hide. Heck, you don’t even need any threading.
1. Create an alias
2. Free the original value
3. Access the alias
If I read it correctly, the variable holding the original value is reset to null after a free but the alias can still access freed memory.
TLDR: Rust has almost no competitors when it comes to the very robust safety guarantees it makes and none when you combine with the performance niche it services.
Programming languages where you are not allowed to access directly any shared variables, but only inside protected data structures, so that complete thread safety is enforced, have existed already a half of century ago, e.g. Concurrent Pascal.
I have not noticed yet anything innovative in this aspect of Rust.
As explained in the article SPARK detects such double free or use after free, even if the standard Ada compiler does not.
The separation between Ada and SPARK in the power of detecting unsafe memory uses is just a market segmentation mechanism, not something intrinsic to the Ada language.
The SPARK development tools must be bought, while the free Ada development tools have less comprehensive error checking.
This is the main disadvantage of Ada vs. Rust. It is a question of money, not of technical qualities.
I think you’ve skipped important words that I’ve said:
> Rust has *almost* no competitors when it comes to the very robust safety guarantees it makes and *none when you combine with the performance niche it services*.
The almost is doing important work in that statement and the none is referring to systems programming. As another commenter noted, SPARK is more than just a cost thing - it fails to scale to non trivial sized projects.
I’m not saying there’s nothing to learn from Ada. All I’m saying is that Rust offers significantly stronger protection and memory safety out of the box than Ada and no language has managed to deliver such memory safety with the performance profile of C and able to target all the same variety of use cases in terms of systems programming (but then also scaling to web services which C/C++ can’t really reach unless you like trivial memory exploits)
> I have not noticed yet anything innovative in this aspect of Rust.
Innovation often times can be subtle like packaging up existing ideas in a friendlier package that can get more mass adoption. If you fail to see the innovation Rust has done with the borrow checker (which afaik is truly novel) and then making the entire language be able to scale from embedded to web services in a cohesive way and also making it a legitimate replacement to C++ in ways that other languages have tried and failed, I think you’ve been too dismissive.
AIUI, SPARK does not use a Rust-like borrow checker: it's based on formal verification which is a lot more difficult to program for, i.e. not really feasible except for smaller programs. This seems to be in sharp contrast to Rust - the safe subset of Rust enforces a set of rules that can actually scale up to larger programs while still preserving safety.
> Ada has its own nomenclature for multithreading: Tasks, and provides its own built-in mechanism for preventing data races between them. Ada's Protected Objects encapsulate data inside an implicit mutex, allowing only one thread access at a time via a public interface.
I believe ADA doesn’t have a guarantee that you are accessing data thread safely. And that lack of guarantee is where use-after-free and double-free can hide. Heck, you don’t even need any threading.
1. Create an alias
2. Free the original value
3. Access the alias
If I read it correctly, the variable holding the original value is reset to null after a free but the alias can still access freed memory.
TLDR: Rust has almost no competitors when it comes to the very robust safety guarantees it makes and none when you combine with the performance niche it services.