1. 22

  2. 2

    Great article! The main areas for improvement in expressiveness might be porting some solvers for something like separation logic to see if stuff they can’t borrow check can pass an automated analysis. Like this (pdf) for SPARK. Looking at her credentials…

    “Claire Dross has a PhD in deductive verification of programs using a satisfiability modulo theory solver with the Universite Paris-Sud. She also has an engineering degree from the Ecole Polytechnique and an engineering degree from the Ecole Nationale Superieure des Telecommunications.”

    …she probably could pull it off if they asked her, too. Three, different universities in engineering is uncommon over here. As a tangent, seeing that makes me wonder if university jumping should be encouraged to accumulate diverse perspectives and broader network of potential collaborators. Alternatively, staying in one spot for long time to accumulate talent and results in a given group as is typical. Worth thinking about.

    1. 2

      Interesting stuff happens at the boundaries. So yes to all those questions.

    2. 2

      For people unfamiliar with Rust, this is the primary difference:

      In addition to single ownership, SPARK restricts the use of access types in several ways. The most notable one is that SPARK does not allow general access types. The reason is that we did not want to deal with accesses to variables defined on the stack and accessibility levels. Also, access types cannot be stored in subcomponents of tagged types, to avoid having access types hidden in record extensions.

      Rust allows both stack references and storing references in structs in exchange for more complex model and increased annotation burden. Both restrictions are probably the right choice for the first version of this support in SPARK though.