[fresh_broccoli]

>1) memory safety at compiler level

Ada isn't memory safe. It doesn't have anything resembling a borrow checker. The spec used to allow an optional garbage collector, but that was never widely used in practice and was removed in Ada 2012. The average production codebase relies on Unchecked_Free/Unchecked_Deallocation for memory management.

I find it genuinely baffling that so many people who praise Ada clearly don't know and/or don't use the language.

[trott]

Yep, and even without dynamic memory management, Ada is not type-safe: https://www.enyo.de/fw/notes/ada-type-safety.html

Rust also has soundness holes, by the way. This one is almost 10 years old: https://github.com/rust-lang/rust/issues/25860

[steveklabnik]

Tons of languages have soundness bugs. While that one is ten years old, there have been zero reports of it ever being found in the wild, and it will finally be fixed relatively soon.

[trott]

> it will finally be fixed relatively soon

2015: "The work needed to close this has not yet landed. It's in the queue though, once we finish up rust-lang/rfcs#1214."

[steveklabnik]

Yes. For various other reasons, the trait system needed to be rewritten, and it would also end up fixing this. Since it’s essentially a theoretical issue, spending time on this wouldn’t make sense. In the meantime, that rewrite is nearing completion. The most recent version of rust uses it for coherence checking. The next few months are likely to remove several other stoppers from moving forward. It’s almost time for a crater run, and then fixing whatever issues that shows up.

[SkiFire13]

The Rust one seems a specific bug in the implementation, while the Agda one seems more like a fundamental flaw caused by allowing aliased mutation though.

[touisteur]

Haven't seen uncheched_deallocation in modern codebases in a long time... The secondary stack removes many/most use cases of short-lived dynamic allocation and pointer-passing. Controlled types, containers, alleviate most other use-cases. I'd frown at code review if I saw raw memory allocation. Memory safety issues I've seen (very rarely in 15 years of dev) hinge on aliasing, stack overflow (which you can mostly catch now) and tumbling down in C bindings.

I'll praise the language I use daily as far more memory-safe than the others I use daily (bar managed-memory Java-like languages).

[AlotOfReading]

Ada/SPARK can be memory safe, in part because they borrowed ideas from Rust.

[0] https://blog.adacore.com/using-pointers-in-spark

[LiamPowell]

You can't have the borrow checker without bringing the rest of SPARK with it as far as I'm aware, so this comes with the requirement that you prove the your program contains no other runtime errors.

[LiamPowell]

Pointers are memory safe as long as Unchecked_Deallocation/Unchecked_Access are never used thanks to how pointers have scopes, even though pointers can be pointing to variables on the stack.

You can go a very long way without ever touching Unchecked_Deallocation compared to C or Rust, even without allowing for use of the standard library where deallocation is done under the hood. I use it rarely enough that I have to go check the package specification every time I need it.

You also have relatively safe deallocation when you wrap your allocation in a storage pool and let RAII deal with it as the pointer system keeps you safe from a dangling reference if your container type only frees memory within the Finalize procedure.

You don't have the complete memory safety of a GC or Rust's borrow checker without SPARK, but you can completely avoid the unsafe parts or use well tested containers as opposed to C and other similar language where you need unsafe pointers to do anything non-trivial.

[caspper69]

Borrow checking is not the only way to achieve memory safety.

[currymj]

i was very careful to use the vague phrasing "features dealing with these problems" and not "Ada has a borrow checker and dependent types".