[aw1621107]

I'm not sure I see much of a difference still. Here's what I think is a more correct Rust comparison:

> In [Rust]: you keep the spec in the verifiable world (a [type checker-visible function signature]) and place the implementation outside the proof boundary (for example in a body or unit compiled with `unsafe`). The body is visible in source but intentionally opaque to the [type checker; callers are still proved against the spec and must rely on that contract.

These "practical differences" seem questionable to me as well.

> Granularity: `unsafe` is lexical (blocks/functions); SPARK's hatch is modular/procedural (spec vs body).

`unsafe` can trivially be expanded from a block to a function body, thereby transforming it to a "modular/procedural" hatch. `unsafe` on function signatures is more akin to SPARK's `Assume`, albeit with the precise assumption (hopefully) in the documentation.

> Visibility: Rust's unchecked code is written inline and annotated with `unsafe`

This... doesn't seem like a difference to me? According to you, you can place SPARK's unchecked code "in a body [] compiled with `pragma SPARK_Mode(Off)`". That sure sounds like writing unchecked code "inline" and annotated with SPARK's equivalent of `unsafe` to me.

> SPARK's unchecked implementation is placed outside the prover but the spec remains visible and provable.

You can say an analogous thing about Rust: The unchecked implementation is placed outside the [type checker] but the [function signature] remains visible and [checkable].

> Enforcement model: Rust's safety holes are enforced/annotated by the compiler's type/borrow rules (caller and callee responsibilities are explicit at the site).

This is... confusing? I'm honestly not sure what you're trying to get at.

> SPARK enforces sound proofs on the interface; the off-proof body must be shown (by review/tests/docs) to meet the proven contract.

The Rust equivalent is a non-`unsafe` function signature with an `unsafe` body, and what you say is equally as applicable.

> Best practice: keep off-proof bodies tiny, give strong pre/postconditions on the SPARK spec, minimize the exposed surface, and rigorously review and test the non-SPARK implementation.

This... doesn't describe a difference at all? It's equally as applicable to the analogous Rust construct.

> `unsafe` = "this code block bypasses language checks"

Technically wrong? Bit of a nitpick, but `unsafe` technically does not disable any language checks; it gives you access to unchecked capabilities. It's a slight difference but an important one, since it means that if you have code that doesn't compile and doesn't use unchecked capabilities (e.g., a borrow checking error with regular references), wrapping the code in `unsafe` will not allow your code to compile.

> SPARK's escape hatch = "this implementation is deliberately outside the prover, but the interface is still what we formally prove against."

Again, you can say basically the same thing for non-`unsafe` functions in Rust.

[johnisgood]

I think you're conflating surface similarity with semantic equivalence - Rust's `unsafe` is not the same as SPARK's off-proof/`SPARK_Mode(Off)` hatch.

> `unsafe` can trivially be expanded from a block to a function body, thereby transforming it to a "modular/procedural" hatch. `unsafe` on function signatures is more akin to SPARK's `Assume`, albeit with the precise assumption (hopefully) in the documentation.

Not exactly. The key difference is semantic, not syntactic. 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.

> This... doesn't seem like a difference to me? According to you, you can place SPARK's unchecked code "in a body [] compiled with `pragma SPARK_Mode(Off)`". That sure sounds like writing unchecked code "inline" and annotated with SPARK's equivalent of `unsafe` to me.

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.

> You can say an analogous thing about Rust: The unchecked implementation is placed outside the [type checker] but the [function signature] remains visible and [checkable].

Not really. Rust enforces type and ownership correctness, not behavioral correctness. SPARK's prover generates semantic proof obligations for each call based on the spec. Rust's function signature alone does not provide that level of guarantee.

> This is... confusing? I'm honestly not sure what you're trying to get at.

The point is that SPARK enforces caller correctness automatically via the prover using the spec. The off-proof body is a separate assurance item. In Rust, `unsafe` transfers responsibility to the implementer; the compiler does not enforce semantic contracts. The difference is enforcement model: SPARK's model gives machine-checked guarantees for safe clients, Rust does not.

> The Rust equivalent is a non-`unsafe` function signature with an `unsafe` body, and what you say is equally as applicable.

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.

To reiterate in a way that may be understood better: without additional external verification, Rust does not automatically prove anything about functional behavior across the `unsafe` boundary. SPARK does, by design: callers are verified against the spec even if the body is off-proof. Rust requires a separate verifier (Prusti, Creusot, Kani, Verus) plus annotations to reach the same level of guarantee[1].

> This... doesn't describe a difference at all? It's equally as applicable to the analogous Rust construct.

Best practices may overlap (small unchecked regions, rigorous review), but that doesn't make them equivalent. SPARK's off-proof body is part of a proof-integrated model; Rust's `unsafe` is merely a compiler capability marker. The guarantees differ.

> Technically wrong? Bit of a nitpick, but `unsafe` technically does not disable any language checks; it gives you access to unchecked capabilities. It's a slight difference but an important one, since it means that if you have code that doesn't compile and doesn't use unchecked capabilities (e.g., a borrow checking error with regular references), wrapping the code in `unsafe` will not allow your code to compile.

Correct, that nuance is valid. It does not change the core distinction though: SPARK produces verifier-checked obligations for the interface, whereas Rust's `unsafe` simply gives the programmer unchecked access without automated semantic proofs.

> Again, you can say basically the same thing for non-`unsafe` functions in Rust.

No. Non-`unsafe` Rust functions are type-safe, but they do not automatically generate semantic verification conditions for callers. SPARK does, and this is the fundamental difference: proof-driven interface vs. capability marker.

TL;DR: SPARK's "escape hatch" is a proof-driven verification boundary: the spec is machine-checked and callers are proved against it; the implementation may be off-proof but the interface guarantees remain enforced. Rust's `unsafe` is a language capability marker that grants low-level operations and transfers responsibility to the programmer; it does not, by itself, produce verifier-checked behavioral contracts (you need external tools like Prusti/Creusot/Kani/Verus for that).

I can re-explain the differences in a more digestible manner if that would help, instead of going back and forth.

[1] See https://news.ycombinator.com/item?id=45508022 as well.

[aw1621107]

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.

[johnisgood]

> I'm quite aware that Rust doesn't have the same ability to verify behavior that SPARK does ... 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.

I understand your point about the structural analogy that in both languages you can have a function body where the usual automated checks are relaxed or treated as opaque. That said, the resemblance is syntactic/structural, not semantic. SPARK's off-proof body is embedded in a proof-driven model: the spec generates verification conditions for callers automatically, and those obligations are enforced by the prover. Rust's `unsafe` merely lifts type/borrow restrictions for the implementer; there are no automatic, prover-enforced obligations for callers, and correctness must be established by review/tests or by external verification tools.

> `unsafe` in the 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".

Structurally, yes, both expose an interface and localize unchecked operations but the enforced guarantees are not comparable. In SPARK, the spec is visible to the prover and the implementation is opaque to the prover; the prover enforces machine-checked contracts for all callers. In Rust, the function body remains visible to `rustc` (and `unsafe` only grants access to unchecked capabilities); the compiler enforces type/ownership rules but does not ensure higher-level behavioral correctness across `unsafe` boundaries. That semantic difference is what makes SPARK "proof-driven" vs. Rust `unsafe` a "capability marker"[1].

TL;DR: They may look analogous at the interface/body level, but only SPARK actually enforces semantic guarantees. `unsafe` is a marker that shifts responsibility to the programmer; it does not create verifier-checked obligations for callers.

[1] By "capability marker" (privileged/block-scoped permission, escape/privilege annotation, whatever) I mean that `unsafe` is an annotation that grants permission to perform low-level/unchecked operations; it does not, by itself, create machine-checked behavioral contracts for callers.

[aw1621107]

I still feel you're missing my point. What you're describing as differences are generally differences between SPARK and Rust, not really a difference between `unsafe` and `SPARK_Mode(Off)`. For example:

> Rust's `unsafe` merely lifts type/borrow restrictions for the implementer

This is a commonality (for respective language constructs), not a difference, since you can just as easily say "`SPARK_Mode(Off)` merely lifts [SPARK] restrictions for the implementer". That is one of the primary reasons both `unsafe` and `SPARK_Mode(Off)` exist!

> there are no automatic, prover-enforced obligations for callers

To the extent that we are considering proof obligations beyond what is expressible in Rust's type system, this is a difference between Rust and SPARK that is completely independent of whether `unsafe` is used or not.

> and correctness must be established by review/tests or by external verification tools.

Again, this is common to both `unsafe` and `SPARK_Mode(Off)`. Neither Rust's compiler nor the SPARK verifier can guarantee that the implementing code covered by `unsafe`/`SPARK_Mode(Off)` actually fulfills the contract specified in the respective interfaces. The onus of doing so is placed on the programmer.

> Structurally, yes, both expose an interface and localize unchecked operations but the enforced guarantees are not comparable.

Again, this is a difference between Rust and SPARK that is independent of the use of `unsafe`/`SPARK_Mode(Off)`, not a difference between `unsafe` and `SPARK_Mode(Off)`.

> `unsafe` is a marker that shifts responsibility to the programmer

And once again, this also applies to `SPARK_Mode(Off)`. Straight from the Ada docs (emphasis added):

> When a non-SPARK completion is provided for a SPARK declaration, the user has an obligation to ensure that the non-SPARK completion is consistent (with respect to the semantics of SPARK) with its SPARK declaration.

That's just like what `unsafe` does in function bodies!

> [1] By "capability marker" (privileged/block-scoped permission, escape/privilege annotation, whatever) I mean that `unsafe` is an annotation that grants permission to perform low-level/unchecked operations; it does not, by itself, create machine-checked behavioral contracts for callers.

I don't see how this doesn't describe `SPARK_Mode(Off)`. You can say "`SPARK_Mode(Off)` is an annotation that grants permission to perform [Ada operations not in the SPARK subset; i.e., "unchecked" operations]."

Furthermore, I don't think anyone is claiming that `unsafe` in function bodies "create[s] machine-checked behavioral contracts for callers" (not to mention `SPARK_Mode(Off)` doesn't do that either). That would be kind of contrary to its purpose, after all.

One other thing:

> In Rust, the function body remains visible to `rustc`

This is wrong in this context. When compiling code rustc looks at function bodies in isolation - i.e., only when compiling that specific function body. Function bodies are opaque in the context of checking function calls - in other words, callee function bodies are not visible to the compiler. The presence or absence of `unsafe` in the function body makes zero difference in how the function signature is treated, just like how `SPARK_Mode(Off)

[johnisgood]

You're right that `unsafe` and `SPARK_Mode(Off)` are structurally analogous escape hatches - both let implementers use operations outside the verified/safe subset. I accept that the VCs-for-callers difference exists whether or not `SPARK_Mode(Off)` is used - it's a SPARK-vs-Rust language difference, not a construct difference.

I was conflating the constructs with their language contexts. The constructs are analogous; the languages are not.

That said: the original thread is comparing Ada/SPARK vs Rust for high-assurance systems, and in that context, the language-level difference is what matters. When you use `SPARK_Mode(Off)`, you still get integrated caller verification. When you use `unsafe`, you don't - you need external tooling. That ecosystem difference drives language choice for formal verification work, even though the constructs themselves are analogous.

[aw1621107]

> That said: the original thread is comparing Ada/SPARK vs Rust for high-assurance systems, and in that context, the language-level difference is what matters.

Sure, and I don't think anyone is generally disputing that Rust and SPARK have different compile-time capabilities. The only point I was trying to make in this specific subthread is that `unsafe` and `SPARK_Mode(Off)` are not as different as you originally claimed.