[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.