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 additio

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 https://blog.adacore.com/using-pointers-in-spark