From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Simon Wright <simon@pushface.org>
Newsgroups: comp.lang.ada
Subject: Re: Rust's temporal safety for Ada/SPARK
Date: Mon, 15 May 2017 20:07:49 +0100
Organization: A noiseless patient Spider
Message-ID: <lyd1bahray.fsf@pushface.org>
References: <cf1c1eb7-61cf-4ee5-8837-d4a95f95a4ba@googlegroups.com>
	<of7t2m$pdb$1@dont-email.me>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: mx02.eternal-september.org;
 posting-host="94583b61ceb897cd6e52f92d45ba4c4e";
	logging-data="29599"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1/m7IgoWr0obPmd44QH1a7q0eb9tFYdr3E="
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.1 (darwin)
Cancel-Lock: sha1:K9/sZDAIA2T02Z+I5yZx3dsjbo8=
	sha1:Zx+yVnU7ncsAnFT/yUVE5qduI7g=
Xref: news.eternal-september.org comp.lang.ada:46788
Date: 2017-05-15T20:07:49+01:00
List-Id: <comp.lang.ada>

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