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 X-Received: by 10.99.157.137 with SMTP id i131mr1523557pgd.78.1494797315161; Sun, 14 May 2017 14:28:35 -0700 (PDT) X-Received: by 10.157.4.34 with SMTP id 31mr58456otc.2.1494797315103; Sun, 14 May 2017 14:28:35 -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!c26no1505502itd.0!news-out.google.com!m134ni610itb.0!nntp.google.com!c26no1503041itd.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Sun, 14 May 2017 14:28:34 -0700 (PDT) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=88.191.144.200; posting-account=T8VIJwoAAAA-IUorDdqOSpjmb16opbau NNTP-Posting-Host: 88.191.144.200 References: User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <47791fc4-87b8-48d7-8d16-3e0407eb9dfe@googlegroups.com> Subject: Re: Rust's temporal safety for Ada/SPARK From: moy@adacore.com Injection-Date: Sun, 14 May 2017 21:28:35 +0000 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Xref: news.eternal-september.org comp.lang.ada:46782 Date: 2017-05-14T14:28:34-07:00 List-Id: [I'm reposting here my answer to your message on ada Reddit.] In fact, we currently have at AdaCore an intern working with us on the incl= usion of Rust-like pointers in SPARK. He has reached a first milestone whic= h was the description of suitable rules to include safe pointers in SPARK, = which have convinced the SPARK Language Design Group at AdaCore and Altran = UK (the small group working on the evolutions of the SPARK language). He's now working with us and researchers from Inria team Toccata to give a = mathematical semantics to the notions that we're using for these safe point= ers: move (on assignment mostly), borrow (on parameter passing for mutable = objects) and observe (on parameter passing for immutable objects). We have = also started looking at the concrete implementation of these rules in GNATp= rove (the SPARK analysis tool). In this work, we don't target everything that the Rust borrow checker does: - we leave accessibility checking (the lifetime checking in Rust) to the co= mpiler, using existing Ada rules, plus some restrictions in SPARK to avoid = the need for dynamic accessibility checks - we leave nullity checking to proof (a Verification Condition will be gene= rated for dereference of possibly null pointers), with the help here of Ada= non-null types that reduce the need for such proofs. Given that pointers a= re always initialized to null in Ada, there is no need to separately deal w= ith initialization. - we ignore the problem of memory leaks (which could be tackled later as an= extension of the current scheme) So the main issue that we really address with this work is the issue of non= -aliasing. Or rather the issue of problematic interferences, when two names= , one of which can be updated, are referring to the same memory location. W= e're focusing on this issue, because it is the one preventing inclusion of = pointers in SPARK, as for formal analysis we rely on the ability to perform= modular analysis, where we make assumptions on the absence of problematic = interferences. But since our solution to non-aliasing is based on this Rust-like notion of= ownership of pointers, the same solution will also forbid use-after-free o= r double-free. This work is ongoing, we will certainly let the community know about our pr= ogress after the summer.