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