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,FREEMAIL_FROM autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 10.129.177.1 with SMTP id p1mr1739561ywh.28.1494707607264; Sat, 13 May 2017 13:33:27 -0700 (PDT) X-Received: by 10.157.4.34 with SMTP id 31mr199755otc.2.1494707607224; Sat, 13 May 2017 13:33:27 -0700 (PDT) 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.glorb.com!l39no787322qtb.0!news-out.google.com!m134ni4343itb.0!nntp.google.com!c26no1286462itd.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Sat, 13 May 2017 13:33:27 -0700 (PDT) Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=73.91.216.22; posting-account=viu8XwoAAAAzhf3NstShw2l2R6SQaaQR NNTP-Posting-Host: 73.91.216.22 User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: Subject: Rust's temporal safety for Ada/SPARK From: digitalkevlar@gmail.com Injection-Date: Sat, 13 May 2017 20:33:27 +0000 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Xref: news.eternal-september.org comp.lang.ada:46773 Date: 2017-05-13T13:33:27-07:00 List-Id: I'm a high-assurance engineer/researcher who mainly evangelizes the use of = proven methods, tools, etc in proprietary and FOSS systems. I've promoted A= da long time (esp Barnes' Safe and Secure book) but I don't use it myself s= o I need help answering something. Inspired by Cyclone language and linear = types, the Rust language has pulled off a rare feat in using the ownership = and type system (esp affine types) to eliminate temporal errors that come f= rom mismanaging references. That plus two "traits" eliminates race conditio= ns, too. This is not in static code or something with heavy restrictions on= what the code can do. Their thriving community is coding about everything = you can think of from desktop (eg Redox OS) to servers (eg TrustDNS) to emb= edded (eg Tock OS). Here's a description of their memory-safety scheme: https://doc.rust-lang.org/book/references-and-borrowing.html Here's the Cyclone page for people just curious where it came from or on sa= fe languages in general: https://en.wikipedia.org/wiki/Cyclone_(programming_language) So, with Rust's approach, they get memory safety even for *dynamic or concu= rrent 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 m= any 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 hav= e Rust's capability to enforce both temporal, memory safety and immunity to= race conditions? I'm really focusing on an equivalent to the borrow-checke= r in Rust, though. If it doesn't have an equivalent, is there anyone workin= g 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, s= o I figure I ask the experts first. Thanks ahead of time. Nick P.