No, you can guarantee much more with regarding to safety using Ada/SPARK. I have a table somewhere. So if you want safety guarantees, it is Ada/SPARK all the way. Check out https://blog.adacore.com.

I cannot emphasize it enough: if people really wanted so much safety, they would have chosen Ada/SPARK. I also find Ada easier to read and write than Rust. I know C, OCaml, Erlang, Forth, and Factor, yet I have difficulties with Rust. Am I really that bad of a programmer? Welp, at least I know Ada and I can write actually super safe stuff. :P

A lot of those guarantees are only available in the alloc-free subset of Ada, which make them much less attractive. The devil is in the details, making Ada guarantees not always better than Rust ones.

Hm, so can Ada/SPARK bring the same memory safety/data race guarantees to the table as Rust, yet not being more difficult to express and maintain those guarantees? I'm not familiar with the language.

No, Ada has no lifetimes and borrow checking and thus cannot possibly offer the same expressiveness as Rust while supporting safe memory deallocation without garbage collection.

You may want to read https://www.adacore.com/uploads/techPapers/Safe-Dynamic-Memo.... It talks plenty about lifetimes and borrowing. It even mentions Rust (and ParaSail).

> The goal is to allow a pattern of use of pointers that avoids dangling references as well as storage leaks, by providing safe, immediate, automatic reclamation of storage rather than relying on unchecked deallocation, while also not having to fall back on the time and space vagaries of garbage collection.

You might also want to read about how Ada/SPARK does safe pointers. An older article that may be of interest: https://blog.adacore.com/using-pointers-in-spark. Check out https://docs.adacore.com/spark2014-docs/html/ug/en/source/ac... as well, there is a section named "Deallocation". GNATprove guarantees the absence of memory leak (pretty good, right?) in the code shown under that section.

This is how the code looks like:

  with Ada.Unchecked_Deallocation;

  procedure Test is
     type Int_Ptr is access Integer;

     procedure Free is new Ada.Unchecked_Deallocation (Object => Integer, Name => Int_Ptr);

     X : Int_Ptr := new Integer'(10);
     Y : Int_Ptr;
  begin
     Y := X;
     Free (Y);
  end Test;

GNATprove output:

  test.adb:8:04: info: absence of memory leak at end of scope proved
  test.adb:9:04: info: initialization of "Y" proved
  test.adb:9:04: info: absence of memory leak at end of scope proved
  test.adb:11:06: info: absence of memory leak proved

Does that proposal allow to express anything that can be expressed in Rust?

That seems quite unlikely given the lack of syntax for lifetimes. It's still in theory possible to infer them, but that would result in API instability and hard to decipher error messages.

Can you for instance have a function that given a reference to an hash table and a reference to a key returns a reference to the value corresponding to a key equal to the given one? (this requires the return value lifetime to be the same as the hash table lifetime, while the search key lifetime is unrelated)

Can you refactor code that takes multiple parameters by reference to taking by value a single structure including those parameters as fields with independent lifetimes?

That is why SPARK exists, and RAII offers safe memory deallocation.

Ada never used GC, although Ada 83 allowed for optional implementation, that no compiler ever made use of, thus it was removed from Ada standard in the 2005 revision.

"I think Ada/SPARK needs to seriously be considered for a lot more projects. Maybe we need better tooling, but still".unwrap().unwrap().unwrap()

It has a package manager now! :D Anyways, there are some things that could make Ada/SPARK more desirable but it has nothing to do with the language itself. :(

> zero runtime overhead due to the burrow checker

You have to structure the program in a way to make it happy, though. Which is not zero runtime overhead compared to a wild west program.

Nope, Rust still cannot provide formal proofs Ada/SPARK style, and using String, Vec, Rc, Arc, RefCell imposes just runtime checks as other type safe systems languages.