Re: Rust's temporal safety for Ada/SPARK

[Niklas Holsti <niklas.holsti@tidorum.invalid>]

On 17-05-14 00:19 , Jeffrey R. Carter wrote:
> 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 agree that Ada accessibility rules are related to Rust's scoped 
lifetimes, but my impression (after a brief read of the Rust 
"borrow-checker" material) is that the Rust scheme goes a lot further 
than what is today standard in Ada. For example, AIUI Rust makes it 
impossible to try to dereference a null pointer, and Rust also 
completely prevents dangling references, even when dynamically allocated 
objects are deallocated.

In a multi-threaded program, again AIUI, Rust statically prevents 
concurrent writes from different threads to the same variable. That is 
"legal" in Ada, but (as discussed in a concurrent thread on "Portable 
memory barriers") Ada has unchecked rules on when such access is 
non-erroneous.

AIUI the Rust scheme is based on (a) compile-time tracking of the set of 
references that refer to a given object, as well as the kind of access 
(read-only, or read-and-write) that each reference allows, and (b) 
wrapping all possibly-null references into "Optional" types (similar to 
Ada's variant records) to hide the "null" values.

It is not clear to me if these Rust advantages bring with them some 
restrictions on the kinds of data structures that a Rust program can 
use, or require some Rust-specific idioms for transforming traditional 
reference-heavy data structures (for example graphs) into Rust form.

I hope "someone" will make an in-depth study of how the advantages of 
the Rust scheme could be imported into Ada. I'm afraid it may be rather 
hard to do, as Rust references are so different from Ada's access values.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .