by aw1621107 | 2025-10-08 14:33:30+00:00
There's a reason I keep saying "analogous" and apparently I didn't explain it well enough. I'm quite aware that Rust doesn't have the same ability to verify behavior that SPARK does, and I'm not trying to argue that `unsafe` is literally equivalent to `SPARK_Mode(Off)` or that Rust is capable of everything that SPARK is. What I'm trying to get at is that `unsafe` is not "meaningfully different" because it serves a similar purpose to `SPARK_Mode(Off)` for the respective language constructs. Or perhaps put another way, my claim is that if Rust hypothetically gained a proof system with appropriate information in its function signatures the way `unsafe` would be used in function bodies would be both pretty much exactly the way it's currently used and also morally equivalent to the way `SPARK_Mode(Off)` is used.

I'm not going to respond directly to most of what you say because most of those responses would basically be "I said 'analogous' for a reason", but there are a few additional notes:

> SPARK's modular/procedural hatch is proof-driven: the spec (pre/postconditions, invariants) remains fully visible to the prover, generating verification conditions for callers. The off-proof body is intentionally opaque and becomes an external assurance artifact. Rust's `unsafe` merely lifts compiler restrictions on the enclosed code; it does not automatically generate proof obligations, regardless of whether it is block- or function-scoped.

The proof bit is missing the point. What I was trying to get at is that `unsafe` in the function body, like `SPARK_Mode(Off)`, does not affect the part of the function that interacts with external code. `SPARK_Mode(Off)` does not affect how the prover uses the spec, and `unsafe` does not affect how rustc uses the function signature. The use of `SPARK_Mode(Off)`/`unsafe` is contained entirely within the function body; i.e., they is "opaque".

> Superficially yes, but the semantics differ. In SPARK, the spec is verified for all callers; the body is hidden but the interface guarantees are enforced. In Rust, the `unsafe` body is visible to the compiler and only relaxes type/borrow checks. No automatic verification of functional behavior occurs across the boundary without external tools.

I'm not sure this is entirely accurate. Again, `unsafe` in a function body does not affect how the compiler uses the function signature in the rest of the program; in this way, `unsafe` works similarly to `SPARK_Mode(Off)` in that "the [function signature] is verified for all callers; the body is hidden but the interface guarantees are enforced". Obviously SPARK can guarantee more than Rust, but I'm not trying to argue otherwise.

> Not quite. Without an external verifier and additional annotations, Rust does not automatically prove functional correctness across an `unsafe` boundary. SPARK's off-proof body still guarantees that callers satisfy the verified spec, which is enforced at compile time.

This is a bad wording on my part; "The Rust equivalent" should have been "The analogous Rust construct". Again, I'm trying to show that `unsafe` is not that different from `SPARK_Mode(Off)` for analogous language constructs.