[johnisgood]

... and formal verification is where Ada / SPARK wins over Rust.

I mean, we can go on but I think it quite ends there, as far as safety goes. :D

There is a reason for why Ada is used in industries that are mission-critical.

> Ada needs a profile that guarantees that code can't be the source of erroneous execution and constrains bounded errors further.

Not really, you can just use Ada / SPARK and it is all checked at compile-time. Look for my comments where I mention Ada.

[debugnik]

Only if SPARK is powerful enough to verify the code you need to write in the first place, which from my experience with SPARK is not a given as soon as access types are involved. Also Rust doesn't need to exclude high level language features just to prove memory safety, whereas SPARK can't even verify any use of controlled types.

If SPARK really were enough, I'd just write all Ada in SPARK of course.

[johnisgood]

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

[debugnik]

> permission/ownership model added to GNATprove in recent years.

So recently that last time I tried Alire failed to install me a version of gnatprove that supported it. I hope next time I try it actually works though, because I do like the semantics they came up with from the examples I'd seen.

> that doesn’t prevent you from using controlled types - you just need to isolate them. [...] `pragma SPARK_Mode(Off)`

No need to elaborate, I know that SPARK_Mode => Off is the SPARK equivalent of unsafe in Rust; that is, regular Ada. So yes, it does exclude controlled types, and trying to twist SPARK's lack of semantics for them into a pro is not a good argument IMO.

[johnisgood]

> SPARK_Mode => Off is the SPARK equivalent of unsafe in Rust

As I said before: structurally, yes - both mark an implementation as opaque to the verifier/compiler. Semantically, though, SPARK is proof-driven: the verified interface still generates obligations for all callers, and the off-proof body is modularized. Rust's `unsafe` lifts restrictions, but does not automatically enforce correctness across the boundary. That distinction is why SPARK can provide whole-program, machine-checked guarantees while `unsafe` only shifts responsibility to the programmer.

... but I have already said this.

[afdbcreid]

There is more than one formal verification library for Rust, although none is as integrated as SPARK I believe.

[johnisgood]

How does that work?

Why can't other languages have a "formal verification library"?

[afdbcreid]

> How does that work?

Usually taking the IR (MIR) from rustc and translating it to a verifier engine/language, with the help of metadata in the source (attributes) when needed. E.g. Kani, Prusti, Creusot and more.

> Why can't other languages have a "formal verification library"?

I don't think there is a reason that prevents that, and perhaps some have, however it turns out that modelling shared mutability formally is really hard, and therefore the shared xor mutable rule in Rust really helps verification.

[johnisgood]

Wouldn't C have such a library already if it really was "possible"? You can turn off strict aliasing.

[debugnik]

Not a library, but it kinda does: Frama-C will formally verify C code using special comments to write the contracts in, and I hear it can prove more pointer properties than SPARK, although it takes more more effort to maintain a Frama-C codebase due to all the other missing language features.

[johnisgood]

Does that mean I can use C + Frama-C so I won't have to use Rust (or Ada / SPARK)? :P

[afdbcreid]

Well, I'm not an expert in formal verifications, but there are such libraries, I listed few of them above, you can go and check them. So it is possible.

C doesn't have the shared xor mutable rule - with strict aliasing or without.

[johnisgood]

I checked them, but I am not convinced and I am not sure why it was brought into this thread.

SPARK has industrial-strength, integrated verification proven in avionics (DO-178C), rail (EN 50128), and automotive (ISO 26262) contexts. Rust's tools are experimental research projects with limited adoption, and they're bolted-on and fundamentally different from SPARK.

SPARK is a designed-for-verification language subset. Ada code is written in SPARK's restricted subset with contracts (Pre, Post, Contract_Cases, loop invariants) as first-class language features. The GNAT compiler understands these natively, and GNATprove performs verification as part of the build process. It's integrated at the language specification level.

Rust's tools retrofit verification onto a language designed for different goals (zero-cost abstractions, memory safety via ownership). They translate existing Rust semantics into verification languages after the fact - architecturally similar to C's Frama-C or VCC (!). The key difference from C is that Rust's type system already guarantees memory safety in safe code, so these tools can focus on functional correctness rather than proving absence of undefined behavior.

Bottom line is that these tools cannot achieve SPARK-level verification for fundamental reasons: `unsafe` blocks create unverifiable boundaries, the trait system and lifetime inference are too complex to model completely, procedural macros generate code that can't be statically verified, interior mutability (`Cell`, `RefCell`) bypasses type system guarantees, and Rust can panic in safe code. Most critically, Rust lacks a formal language specification with mathematical semantics.

SPARK has no escape hatches, so if it compiles in SPARK, the mathematical guarantees hold for the entire program. SPARK's formal semantics map directly to verification conditions. Rust's semantics are informally specified and constantly evolving (async, const generics, GATs). This isn't tooling immaturity though, it's a consequence of language design.