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!feeder.eternal-september.org!news.swapon.de!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail From: Niklas Holsti Newsgroups: comp.lang.ada Subject: Re: Rust's temporal safety for Ada/SPARK Date: Sun, 14 May 2017 13:19:53 +0300 Organization: Tidorum Ltd Message-ID: References: Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit X-Trace: individual.net 9ddnJ14A7Ntms3uiHh8A/ABBz/W6rljdwRfeFtPRRfHdSGweVN Cancel-Lock: sha1:9k0tPUMAb2ORpXrV2Zs0eS2rKGg= User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:45.0) Gecko/20100101 Thunderbird/45.8.0 In-Reply-To: Xref: news.eternal-september.org comp.lang.ada:46776 Date: 2017-05-14T13:19:53+03:00 List-Id: 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 . @ .