5 ms·

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 `u

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)

deleted 1y ago
[deleted]
johnisgood 1y ago
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 1y ago
  > 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.

deleted 1y ago

[deleted]

johnisgood 1y ago

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 1y ago
> 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.