Proof of code with pointers now possible in SPARK using pledges

SPARK is a subset/superset of Ada. That is, the code is compiled using usual Ada rules, but to pass the SPARK verification checks requires passing some additional rules. Ada's access types (pointers) are traditional; to use access types within SPARK requires some addition rules, which are lifetime rules.

The "previous post" mentioned in the original article goes into this some more:

https://blog.adacore.com/using-pointers-in-spark

Hi, the SPARK is an industrial-grade toolsuite around an actual specified language, used in actual real-world applications. Since it's a subset of Ada, it's completely integrable in an Ada project. The idea is that you'd have parts of your project in Ada (with all its static and runtime guarantees) and parts in SPARK (and here you also have latitude in which level of proof you want in which part of your code: absence of runtime errors, functional properties, full spec proof...). The SPARK people really thought about the adoption path from Ada (even C) to SPARK.

And they are purely pragmatic: the subset of Ada that constitutes SPARK is the actual subset that is actually tractable to proof.

So they're adding pointers and proofs with pointers using a rust-like ownership model, the SPARK subset will be updated to pointers (yay that was missing).

This is actually an incredible achievement.

I also think all these 'ownership' checks might trickle into Ada later on, and improve static checks without going to proof.

Exciting time to be working with Ada!