|
|
|
|
|
|
by debugnik
255 days ago
|
|
|
> permission/ownership model added to GNATprove in recent years. So recently that last time I tried Alire failed to install me a version of gnatprove that supported it. I hope next time I try it actually works though, because I do like the semantics they came up with from the examples I'd seen. > that doesn’t prevent you from using controlled types - you just need to isolate them. [...] `pragma SPARK_Mode(Off)` No need to elaborate, I know that SPARK_Mode => Off is the SPARK equivalent of unsafe in Rust; that is, regular Ada. So yes, it does exclude controlled types, and trying to twist SPARK's lack of semantics for them into a pro is not a good argument IMO. |
|
|
As I said before: structurally, yes - both mark an implementation as opaque to the verifier/compiler. Semantically, though, SPARK is proof-driven: the verified interface still generates obligations for all callers, and the off-proof body is modularized. Rust's `unsafe` lifts restrictions, but does not automatically enforce correctness across the boundary. That distinction is why SPARK can provide whole-program, machine-checked guarantees while `unsafe` only shifts responsibility to the programmer.
... but I have already said this.