HackerPapers

arXiv:1805.05576cs.PL

Borrowing Safe Pointers from Rust in SPARK

Georges-Axel Jaloyan, Yannick Moy, Andrei Paskevich

Abstract

In the field of deductive software verification, programs with pointers present a major challenge due to pointer aliasing. In this paper, we introduce pointers to SPARK, a well-defined subset of the Ada language, intended for formal verification of mission-critical software. Our solution uses a permission-based static alias analysis method inspired by Rust's borrow-checker and affine types, and enforces the Concurrent Read, Exclusive Write policy. This analysis has been implemented in the GNAT Ada compiler and tested against a number of challenging examples. In the paper, we give a formal presentation of the analysis rules for a miniature version of SPARK and prove their soundness. We discuss the implementation and compare our solution with Rust.

arXiv comments
17 pages, 0 figures
Journal reference
DOI
Subjects
cs.PLProgramming Languages

On Hacker News

Linked by 2 identifiable commenters in 3 comments across 3 threads, from Jul 2020 to Apr 2026. Found in 1 HN submission from Aug 2018 to Aug 2018. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments3 threads

  1. Ada, its design, and the language that built the languages 1 comment

    • The SPARK subset of Ada^1 has a similar kind of move semantics for pointer types^2. 1: SPARK is a formally verifiable subset of Ada: https://en.wikipedia.org/wiki/SPARK_(programming_language) 2: https://arxiv.org/pdf/1805.05576

      ajxsView on HNParent context

  2. Summary After Four Months with Ada 1 comment

    • You might be interested in this thread from a year ago, where we discussed memory management in Ada. [0] The Ada folks sometimes seem a bit quiet on memory-management questions, a bit like the way Forth folks rarely talk about the real-world performance of Forth interpreters. On…

      MaxBarracloughView on HNParent context

  3. Dafny: Verification-Aware Programming Language 1 comment

    • It wasn't a mistake for Rust not to emphasise formal verification. Going that route would have been very restrictive. Rust is aiming to offer a safer alternative to C, not a more approachable formally verifiable language. That said, it looks like the good ideas from Rust may…

      MaxBarracloughView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.