[aw1621107]

> 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]

> 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]

> 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]

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]

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]

You're correct on the technical details: Pre/Post/Type_Invariant were added in Ada 2012, and Global/Depends are SPARK-specific annotations. Fair enough.

But saying "SPARK first appeared in 2009" is incorrect. SPARK dates to the mid-1980s at the University of Southampton.[1][2][3] SPARK was already in industrial use by the early 1990s, selected for Risk Class 1 systems on the Eurofighter programme.[3] The 2009 date is when Praxis/AdaCore released SPARK Pro under GPL[4] - that's commercialization, not creation.

This completely undermines your [irrelevant] evolution argument. SPARK didn't appear after Ada 2012 added contracts. It existed 25 years before them using special comments. When Ada 2012 added contracts, SPARK adopted the native syntax.

And there's no sleight of hand. My original comment explicitly said "Ada / SPARK" - not Ada alone. When discussing safety-critical development, you use them together. That's the deployed ecosystem.

Whether Ada's contract syntax was in the 1983 spec or added in 2012 is irrelevant. Ada 83 was designed for safety-critical embedded systems with strong typing, clear semantics, and explicit data flow - design goals that made formal verification feasible. That's why SPARK could exist starting in 1987.

The practical reality is that Ada/SPARK provides production-ready formal verification with qualified toolchains for DO-178C, EN-50128, and ISO 26262. Rust has experimental research projects (Prusti, Verus, Creusot, Kani) with no certification path and limited industrial adoption. SPARK-level formal verification in Rust is largely theoretical - Rust's design (unsafe blocks creating unverifiable boundaries, no formal specification, evolving semantics, procedural macros, interior mutability) makes whole-program certifiable verification structurally impossible, not just immature. It's almost a dream at this point.

[1] B.A. Carre and T.J. Jennings, "SPARK - The Spade Ada Kernel", University of Southampton, 1988, https://digital-library.theiet.org/content/journals/10.1049/...

[2] B. Carre and J. Garnsworthy, "SPARK - an annotated Ada subset for safety-critical programming", TRI-ADA 1990, https://dl.acm.org/doi/10.1145/255471.255563

[3] https://cacm.acm.org/research/co-developing-programs-and-the...

[4] https://www.adacore.com/press/spark-pro

[aw1621107]

> But saying "SPARK first appeared in 2009" is incorrect.

Yes, you're correct and that claim of mine is wrong. Sorry about that. The reason I claimed 2009 is that that is what Wikipedia said and I couldn't easily find sources saying otherwise. You seem to have had more success in finding good sources, although your source link for [1] seems to be wrong?

> The 2009 date is when Praxis/AdaCore released SPARK Pro under GPL

Not exactly sure that this is where the Wikipedia article pulled the date from. Any reasonable reading should conclude that this is not the same thing as when SPARK "first appeared" and the Wikipedia page doesn't have a citation for that date.

> This completely undermines your [irrelevant] evolution argument.

Not really? Consider again what I said:

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

I think this comment would still be applicable if you change "2009" to "1988"/"1990"/etc. Keep in mind that this comment was in response to your claim that "it's entirely relevant that Ada's design includes verification primitives that Rust lacks" where "verification primitives" were contract facilities, so no matter if SPARK were developed in 2009 or 1988/1990 it would still have been developed before Ada gained contracts.

Somewhat of a sidenote, but your wording seems to imply you have two of my arguments mixed up? The only place I said "irrelevant" has nothing to do with where I discussed evolution, so it's unclear to me why you inserted "irrelevant". Unless it's commentary on my evolution argument, in which case it seems needlessly confusing?

> SPARK didn't appear after Ada 2012 added contracts.

I never claimed that?

> It existed 25 years before them using special comments. When Ada 2012 added contracts, SPARK adopted the native syntax.

Yes, and I said just that. The reason that is an important distinction is because before SPARK 2014 adopted contracts it was "just" an external tool - i.e., "[Ada] requires external tools and annotations to achieve [formal verification]."

> And there's no sleight of hand. My original comment explicitly said "Ada / SPARK" - not Ada alone.

The sleight of hand is the change of topic, not the exact words you used.

> Whether Ada's contract syntax was in the 1983 spec or added in 2012 is irrelevant.

It's relevant because you explicitly claimed "Ada was designed with verification in mind (built-in contracts)". When contracts were added directly impacts the accuracy of your claim - if contracts were added later, then it obviously cannot have been originally designed for verification using contracts.

> Ada 83 was designed for safety-critical embedded systems with strong typing, clear semantics, and explicit data flow

OK, so now we're (sort of) getting to what the comment I originally responded to should have been about! How do those compare against what Rust offers? I think it's easy to claim that Rust also has strong typing. The other two items are a bit vague, but I think there could be an argument that Rust has the third item and depending on what exactly you mean by the second it either can already exist (if you stick to well-defined parts of the language) or nothing prevents it from existing in the future (if you're talking about a formal spec, in which case I'd also argue that the existence of a formal spec is generally independent of the design of a language).

Good further discussion might involve looking at the Ada 83 rationale to see if you can find support for a claim that it was designed for verification. It's a fair bit of text to look through and interpret and a quick search didn't turn up anything obvious, but you might be better equipped to handle that than me.

> Rust's design (unsafe blocks creating unverifiable boundaries, no formal specification, evolving semantics, procedural macros, interior mutability) makes whole-program certifiable verification structurally impossible, not just immature. It's almost a dream at this point.

And here again you're comparing Rust and SPARK instead of Rust and Ada! The former comparison is entirely uninteresting because it's basically a tautology - SPARK intentionally excludes the parts of Ada that it can't formally verify, so obviously the stuff that remains is well-suited for formal verification.

Seriously, consider an Ada analogue:

> Ada's design (access types, side effects in expressions, aliasing etc.) makes whole-program certifiable verification structurally impossible, not just immature. It's almost a dream at this point.

And yet SPARK was able to make formal verification work for Ada by excluding those unverifiable constructs (and in fact later added (partial?) support for one of them back in, inspired by Rust!). Why would a similar operation not be possible for Rust (especially given the fact that verification tools for Rust already exist)

Not to mention the argument is not entirely consistent either. SPARK has "[`SPARK_Mode(Off)`] creating unverifiable boundaries" (i.e., the verifier can't check the "boundary" between spec and implementation). The lack of a formal specification is not a "design" issue, it's a prioritization issue. Nothing prevents Rust from gaining a formal spec in the future, and indeed that work is already taking place, both via prose (e.g., the work done by Ferrocene) and via a real formal spec (e.g., MiniRust). "Evolving semantics" is a bit vague for me to discuss in too concrete terms - on one hand, there's parts of Rust where "evolving semantics" is wrong (consider Rust's backwards compatibility and the edition mechanism), and parts of Rust where "evolving semantics" is correct in two different ways (gaining new capabilities/semantics vs. deciding how to deal with generally underspecified bits of the language). SPARK can also be said to have "evolving semantics" since it gains new capabilities over time, but I suspect that's not what you meant.