Why doesn't Ada/SPARK have lifetimes?

General
1

Hope this doesn’t sound too dumb, but why doesn’t SPARK have explicit lifetimes like rust does?
Does SPARK just assume what your lifetimes are and proves them for you?

2

In Ada, there are several things that play into this, first:

  1. Local declarations; because Ada allows return-values of complex types, like unconstrained arrays, this tends to alleviate much of the need for accessed (pointers), combined with the modes in, out, in out and the ability to use same unconstrained arrays as parameter-types, this virtually eliminates the need for pointers.
  2. Generic — Because generics can have subprograms and objects (of modes in or in out) you can directly reference [possibly mutably] an item without having to use pointers.
  3. Type lifetimes; likewise (and because nested packages/declare-blocks are useful), we know that an access-type’s existence (and therefore all values of that type) can only be, at most, that of the type it accesses. — Therefore, Ada implementations are given permission to free all accesses whose type goes out of scope.

In short, Ada uses ‘lifetimes’ differently (more type-centric and structural) than you’re thinking (scope of a pointer), and as one programmer likes to say about Ada: “To a first order approximation: you never need access types in Ada.”

3

This maybe?

4

There’s a rationale for this in the paper Recursive Data Structures in SPARK (in the “Related Work” section):

The ownership rules introduced in SPARK are largely inspired by the Rust language [11]. The differences are mostly motivated by the need to comply with the preexisting Ada semantics of pointers. In addition, SPARK was aiming at coming up with a subset as easy to verify as possible. The resulting model is simpler because it does not make lifetime of borrowers explicit, and aliases created through borrows are always statically known.

5

I very much agree with this, but it’s really hard to describe this to people. I use like 1/100th the number of pointer-like things in Ada versus C++ since I don’t have to manually do const T& for “class-likes” (limited or tagged).

Access types aren’t “just” pointers, they also carry their accessibility with them. Overall, Ada has “accessibility rules”, which are a sort of primordial concept of lifetime. An access type is sort of assumed to have the lifetime of the entirely program scope in which it’s visible, if it’s in a package, then it’s lifetime encompasses all places that type is visible. If you point at an object which has a lifetime shorter than that you get a compile-time error and are forced to use 'Unchecked_Access.

Accessibility is… complicated. That part of the spec has a note calling it “The Heart of Darkness.” Not all rules can be checked statically, so sometimes there are runtime checks inserted. :cry:

Ada has (to me) two types of access types: “storage pool”, (i.e. usually heap only) (type T is access Integer) and “anywhere”, heap OR stack (type T is access all Integer). Pointers are also nominally typed, not structurally typed, like in Rust/C/C++. There’s also “access parameters”, but I’m a bit fuzzy in that area and leave it to folks who don’t just write “fun and fluffy Ada” like me.

type Foo is access all Integer;
type Bar is access all Integer;

--  ...

F : Foo := new Integer'(5);
B : Bar := new Integer'(6);
F : Foo := B;  --  COMPILE ERROR

Note also that you cannot point to anything on the stack unless it’s aliased:

Fail : Integer;
OK : aliased Integer;

-- ...

F := Fail'Access;  -- COMPILE ERROR, not aliased
F := OK'Access;   -- OK

This applies also to parameters:

procedure ABC (U : Integer; V : aliased Integer) is
   G : Foo := U'Access;  -- COMPILE ERROR
   H : Foo := V'Access;  -- sort of OK... pretty sure actually need 'Unchecked_Access here because of accessbility rules
begin
   -- ...
end ABC;

This is because things that look like they’re “on the stack” aren’t guaranteed to even have an address! (they could be optimized into a register). You also cannot point to an element of a record unless it’s marked as aliased.

If we want to use a pointer temporarily, we can just do that, and the type doesn’t escape the subprogram:

procedure Another (V : aliased in out Integer) is
    type Int_Ptr is  access all Integer;  -- Int_Ptr type is only visible inside this subprogram
    My_Ptr : Int_Ptr := V'Access; -- OK
begin
   -- ... 
end Another;