3 ms·

> However, it is misleading to claim Rust is plainly more amenable to formal verification than Ada. SPARK is a deliberately restricted subset of Ada designed fr

> However, it is misleading to claim Rust is plainly more amenable to formal verification than Ada. SPARK is a deliberately restricted subset of Ada designed from the ground up for static proof Hold on, there's some slight of hand going on here. The person you're responding to was comparing Rust and Ada, both languages not intentionally originally designed for formal verification. You, on the other hand, are comparing Rust, a language that was not originally designed for formal verification, and Ada/SPARK, which is designed for formal verification by definition. That's not a proper comparison for what GP was claiming! A correct comparison would probably involve identifying "a deliberately restricted subset of [Rust] designed from the ground up for static proof" and comparing its capabilities against what SPARK offers as well as (somehow) comparing how "easy"/"hard" producing that subset was compared to defining SPARK from Ada.

johnisgood 1y ago
> Hold on, there's some slight of hand going on here. [...] A correct comparison would probably involve identifying "a deliberately restricted subset of [Rust] designed from the ground up for static proof" and comparing its capabilities against what SPARK offers as well [...] I understand your point, comparing a hypothetical Rust subset specifically designed for formal verification to SPARK is a fairer apples-to-apples framing. My earlier point was contrasting full Rust and SPARK to highlight that SPARK’s integrated, industrial-strength proof model is unmatched in terms of whole-program, auditable guarantees. Rust's ownership and borrow system indeed provides leverage for verification tools, and subsets verified with Prusti, Creusot, Kani, or Verus can achieve interesting results. However, the structural design of Rust (unsafe blocks, interior mutability, macros, undefined behavior, evolving semantics) means that these subsets require careful annotations and external verification; they do not automatically produce the same machine-checked, whole-program, caller-verified obligations that SPARK/Ada guarantees today. TL;DR: Yes, restricted Rust subsets can be verified and are amenable to research-level proofs, but SPARK provides industrial-strength, auditable, whole-program proofs by design, which Rust cannot replicate without extensive external tooling. The comparison isn't about Rust being "bad" at verification - it's about the integrated guarantees SPARK provides that Rust's language design fundamentally does not. The takeaway for the readers here is that SPARK's off-proof body is like a verified contract with an opaque implementation; Rust's unsafe body is like a permission slip that gives the programmer access without automatic enforcement.
- aw1621107 1y ago
  > My earlier point was contrasting full Rust and SPARK to highlight that SPARK’s integrated, industrial-strength proof model is unmatched in terms of whole-program, auditable guarantees. Sure, but that's basically entirely unrelated to what the person you're replying to said, since they were specifically talking about Ada, not SPARK. I don't think anyone is disputing that a language not originally designed for formal verification is comparable to a language that is, and that kind of comparison isn't really interesting because it's apples and oranges.
  - johnisgood 1y ago
    To be honest, I disagree that this is sleight of hand. Ada itself includes contracts (pre/postconditions, type invariants, Global/Depends annotations) as first-class language features. These work at runtime in full Ada and are verified statically in SPARK. Rust has no comparable built-in contract system. So when comparing "Ada vs Rust" for formal verification, it's entirely relevant that Ada's design includes verification primitives that Rust lacks. SPARK isn't a separate language - it's a subset of Ada that leverages Ada's existing contract features for static proof. The contracts are part of Ada whether you use SPARK or not. The GP's claim about Rust being "more amenable to formal verification" ignores that Ada was designed with verification in mind (built-in contracts), while Rust requires external tools and annotations to achieve similar capabilities. That's not apples-to-oranges; it's the core architectural difference between the languages.
    - aw1621107 1y ago
      The sleight of hand was changing a comparison of Rust and Ada to a comparison of Rust and SPARK. If you had actually compared Rust and not-SPARK Ada then as in this comment here, I probably wouldn't have said anything. That being said, now that I'm spending time on this anyways I think there's still at least a few bits of nuance... > Ada itself includes contracts (pre/postconditions, type invariants, Global/Depends annotations) as first-class language features. For what it's worth, I believe none of these features were part of the first few Ada specifications. As far as I can tell, Pre, Post, and Type_Invariant (and design-by-contract features in general) were added in Ada 2012. In a similar vein, Global/Depends annotations appear to be SPARK features (!), so as explained above they're basically irrelevant for a Rust vs. non-SPARK Ada comparison. Why does this matter? SPARK first appeared in 2009, before the features you reference were added to Ada. I think it's a some interesting discussion to be had as to the extent Ada was originally designed to be amendable to formal verification as opposed to how much it evolved to be amendable to formal verification - and in the case of the latter, to what extent Rust could evolve in a similar manner. And kind of piggy-backing off of that: > SPARK isn't a separate language - it's a subset of Ada that leverages Ada's existing contract features for static proof. My understanding is that current SPARK uses Ada's contract features, but since SPARK released before said contract features existed in Ada special comments were used for earlier versions of SPARK instead, which effectively means that before SPARK 2014 Ada "require[d] external tools and annotations" for formal verification. > ignores that Ada was designed with verification in mind (built-in contracts) As stated above, built-in contracts were added to Ada, which means that by definition Ada was not originally designed with those features.

johnisgood 1y ago

> Hold on, there's some slight of hand going on here. [...] A correct comparison would probably involve identifying "a deliberately restricted subset of [Rust] designed from the ground up for static proof" and comparing its capabilities against what SPARK offers as well [...] I understand your point, comparing a hypothetical Rust subset specifically designed for formal verification to SPARK is a fairer apples-to-apples framing. My earlier point was contrasting full Rust and SPARK to highlight that SPARK’s integrated, industrial-strength proof model is unmatched in terms of whole-program, auditable guarantees. Rust's ownership and borrow system indeed provides leverage for verification tools, and subsets verified with Prusti, Creusot, Kani, or Verus can achieve interesting results. However, the structural design of Rust (unsafe blocks, interior mutability, macros, undefined behavior, evolving semantics) means that these subsets require careful annotations and external verification; they do not automatically produce the same machine-checked, whole-program, caller-verified obligations that SPARK/Ada guarantees today. TL;DR: Yes, restricted Rust subsets can be verified and are amenable to research-level proofs, but SPARK provides industrial-strength, auditable, whole-program proofs by design, which Rust cannot replicate without extensive external tooling. The comparison isn't about Rust being "bad" at verification - it's about the integrated guarantees SPARK provides that Rust's language design fundamentally does not. The takeaway for the readers here is that SPARK's off-proof body is like a verified contract with an opaque implementation; Rust's unsafe body is like a permission slip that gives the programmer access without automatic enforcement.

aw1621107 1y ago
> My earlier point was contrasting full Rust and SPARK to highlight that SPARK’s integrated, industrial-strength proof model is unmatched in terms of whole-program, auditable guarantees. Sure, but that's basically entirely unrelated to what the person you're replying to said, since they were specifically talking about Ada, not SPARK. I don't think anyone is disputing that a language not originally designed for formal verification is comparable to a language that is, and that kind of comparison isn't really interesting because it's apples and oranges.
- johnisgood 1y ago
  To be honest, I disagree that this is sleight of hand. Ada itself includes contracts (pre/postconditions, type invariants, Global/Depends annotations) as first-class language features. These work at runtime in full Ada and are verified statically in SPARK. Rust has no comparable built-in contract system. So when comparing "Ada vs Rust" for formal verification, it's entirely relevant that Ada's design includes verification primitives that Rust lacks. SPARK isn't a separate language - it's a subset of Ada that leverages Ada's existing contract features for static proof. The contracts are part of Ada whether you use SPARK or not. The GP's claim about Rust being "more amenable to formal verification" ignores that Ada was designed with verification in mind (built-in contracts), while Rust requires external tools and annotations to achieve similar capabilities. That's not apples-to-oranges; it's the core architectural difference between the languages.
  - aw1621107 1y ago
    The sleight of hand was changing a comparison of Rust and Ada to a comparison of Rust and SPARK. If you had actually compared Rust and not-SPARK Ada then as in this comment here, I probably wouldn't have said anything. That being said, now that I'm spending time on this anyways I think there's still at least a few bits of nuance... > Ada itself includes contracts (pre/postconditions, type invariants, Global/Depends annotations) as first-class language features. For what it's worth, I believe none of these features were part of the first few Ada specifications. As far as I can tell, Pre, Post, and Type_Invariant (and design-by-contract features in general) were added in Ada 2012. In a similar vein, Global/Depends annotations appear to be SPARK features (!), so as explained above they're basically irrelevant for a Rust vs. non-SPARK Ada comparison. Why does this matter? SPARK first appeared in 2009, before the features you reference were added to Ada. I think it's a some interesting discussion to be had as to the extent Ada was originally designed to be amendable to formal verification as opposed to how much it evolved to be amendable to formal verification - and in the case of the latter, to what extent Rust could evolve in a similar manner. And kind of piggy-backing off of that: > SPARK isn't a separate language - it's a subset of Ada that leverages Ada's existing contract features for static proof. My understanding is that current SPARK uses Ada's contract features, but since SPARK released before said contract features existed in Ada special comments were used for earlier versions of SPARK instead, which effectively means that before SPARK 2014 Ada "require[d] external tools and annotations" for formal verification. > ignores that Ada was designed with verification in mind (built-in contracts) As stated above, built-in contracts were added to Ada, which means that by definition Ada was not originally designed with those features.