I've noticed a pattern that many Ada advocates on HN don't really seem to know the language. So they often conflate SPARK with Ada (as you just did) and make unfounded claims about Ada's memory safety, portraying it as being on par with Rust.

It isn't on par, Ada has no lifetime management whatsoever. It doesn't even provide C++ style smart pointers out of the box. It is possible to implement something like shared_ptr, AdaCore even has a tutorial[1], but as the other commenter pointed out, the language doesn't provide the primitives necessary for unique_ptr.

SPARK does have something like this. In fact, in SPARK, every pointer assignment transfers the ownership. But SPARK and Ada aren't synonymous. SPARK is a formal verifier built on top of Ada. Like most such tools, it's very constraining and time-consuming. It's not something that every (or even most) Ada projects use.

Nevertheless, Ada is a perfectly good language, and it's probably safer than C++. It has some really cool features. I'm really fond of in/inout/out references (cppfront stole this), named function parameters, secondary stack, fine-grained control over records (struct) layout, etc.

However, I'm not so fond of the extreme verbosity. It isn't just because of Algol-like keywords, Pascal is less verbose than Ada. Even basic stuff like instantiating generics is very noisy:

   procedure do_something is
     package Integer_Vectors is new
       Ada.Containers.Vectors
         (Index_Type   => Natural,
          Element_Type => Integer);

       vec : Integer_Vectors.Vector;
     begin
       return;
     end;

In C++ that would be:

    void
    do_something(int arg) {
        std::vector<int> vec;
    }

[1] - https://www.adacore.com/gems/gem-97-reference-counting-in-ad...