Re: Rust's temporal safety for Ada/SPARK

[Simon Wright <simon@pushface.org>]

"Jeffrey R. Carter" <spam.jrcarter.not@spam.not.acm.org> writes:

> On 05/13/2017 10:33 PM, digitalkevlar@gmail.com wrote:
>>
>> So, with Rust's approach, they get memory safety even for *dynamic or
>> concurrent use* of memory at compile time with no overhead, runtime
>> checks, GC, etc. Whereas, the last thing I read on Ada showed it has
>> a few tricks but many dynamic uses resort to unsafe deallocations at
>> some point. Other people were suggesting reference counting or a GC
>> leading me to further think it lacks this ability of Rust. So, my
>> question is, does Ada 2012 currently have Rust's capability to
>> enforce both temporal, memory safety and immunity to race conditions?
>> I'm really focusing on an equivalent to the borrow-checker in Rust,
>> though. If it doesn't have an equivalent, is there anyone working on
>> adding it to Ada esp at AdaCore? What Ada/SPARK have already + memory
>> safety for dynamic code would be an awesome combination that would
>> put Rust in distant second. I may be misunderstanding Ada's
>> capabilities, though, so I figure I ask the experts first. Thanks
>> ahead of time.
>
> This looks sort of like Ada's accessibility levels and accessibility
> rules, from ARM 3.10.2, though as it says there, "In most cases,
> accessibility is enforced at compile time by Legality Rules. Run-time
> accessibility checks are also used, since the Legality Rules do not
> cover certain cases involving access parameters and generic packages."

I was thinking that an alternative subject area might be code like

      procedure Add (Dest : in out Integer; N : Integer)
        with
          Post => Dest = Dest'Old + N;

      procedure Add (Dest : in out Integer; N : Integer)
      is
      begin
         Dest := Dest + N;
      end Add;

      Dest : Integer := 42;

   ...
   
      Add (Dest, Dest);

(where we have alternate paths to the variable Dest); but SPARK is happy
and the runtime check isn't triggered, so I suppose the ARM supports
this (by copy-out?).

Still, the usage shouldn't pass code review, I think.