by aw1621107 | 2025-10-08 23:20:58+00:00
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)