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