You're partly right that SPARK is conservative, but the claim that it "can't handle access or controlled types" is misleading.

SPARK does support Ada access types (pointers) under a formal permission/ownership model added to GNATprove in recent years. This system - drawn from Rust's borrow-checker ideas - enforces a Concurrent Read, Exclusive Write (CREW) discipline. It enables verification of typical pointer-based structures (singly-linked lists, trees, other acyclic data) via ownership transfers and borrows that the prover can reason about automatically[1]. So long as you follow the ownership rules (no uncontrolled aliasing, no cycles), GNATprove can verify pointer-based code, ensuring the absence of memory leaks and dangling references.

As for controlled types, SPARK excludes them in the verifiable subset because `Initialize`, `Adjust`, and `Finalize` introduce implicit operations that complicate sound reasoning for the automated prover[2]. However, that doesn’t prevent you from using controlled types - you just need to isolate them. The standard pattern is to define them in a `private` part under `pragma SPARK_Mode(Off)` and expose only SPARK-safe wrappers[3]. The controlled operations still run at runtime, but they are hidden from the proof engine. This way, you retain deterministic finalization and prove correctness for the SPARK-visible interface.

In short: SPARK doesn't "exclude high-level features just to prove memory safety" - it modularizes them. It restricts what the prover sees so proofs remain sound and automatic, but you can still use these features through encapsulation. Rust enforces memory safety through its type system at compile time; SPARK aims to prove memory safety plus richer functional properties (absence of runtime errors, contractual correctness) via formal verification. Their goals differ, and SPARK's restrictions are a deliberate trade-off that enable stronger, machine-checked guarantees for high-assurance software.

If you want me to elaborate on the specifics, let me know. Additionally, see https://news.ycombinator.com/item?id=45494263.

Additionally, I am willing to provide more information about what SPARK typically can prove automatically and why some gaps exist.

[1] Jaloyan, Moy, Paskevich - Borrowing Safe Pointers from Rust in SPARK (permission-based alias analysis)

[2] SPARK 2014 User’s Guide, Language Restrictions (implicit operations, excluded features)

[3] AdaCore SPARK tutorials/blogs - exposing controlled types behind SPARK-safe interfaces