Re: Rust's temporal safety for Ada/SPARK

["Jeffrey R. Carter" <spam.jrcarter.not@spam.not.acm.org>]

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."

-- 
Jeff Carter
"Well, a gala day is enough for me. I don't think
I can handle any more."
Duck Soup
93