Re: Rust's temporal safety for Ada/SPARK

[moy@adacore.com]

[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 inclusion of Rust-like pointers in SPARK. He has reached a first milestone which 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 pointers: 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 GNATprove (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 compiler, 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 generated 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 are always initialized to null in Ada, there is no need to separately deal with 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. We'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 or double-free.

This work is ongoing, we will certainly let the community know about our progress after the summer.