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

[johnisgood]

You made several good points. I agree with some of them and I think the remainder is a matter of framing. Below is a hopefully direct, precise reply that (a) acknowledges the valid objections, (b) restates the crux of your original argument cleanly, and (c) points the discussion toward the practical/architectural distinction that matters for verification and certification.

Chronology does not overturn the substantive claim I was making. My position is not: "SPARK is merely an older tool and therefore superior".

My position is:

  1. Ada and SPARK represent a continuous, coherence-of-purpose: Ada was designed from early on for high-integrity, safety-critical systems (strong typing, conservative semantics, explicitness) and SPARK is the engineering of that design into a verifiable subset and toolchain. SPARK was not an afterthought bolted on to make Ada proveable; it is the outgrowth of Ada's long-standing high-integrity philosophy and of work done in the 1980s/1990s to make that philosophy formally checkable[1][2][3][4][5].
  
  2. The practical distinction that matters in real-world certification and high-assurance engineering is not merely "does the language have an escape hatch" or "did a verification subset exist earlier or later". It is: does the language + toolchain provide an integrated, auditable, certifiable workflow that produces machine-checked caller-facing proofs and supplier artifacts acceptable to certification authorities today? SPARK + GNATprove + Ada toolchain do that now. The Rust ecosystem offers "promising" research tools and engineering efforts, but it does not yet provide the same integrated, certification-proven toolchain and supplier artifacts out of the box.

  3. From an academic or R&D viewpoint, your point about "you could build a Rust subset with verification primitives" is correct and constructive: people are doing exactly that. But the practical, operational gap between "research-verified components" and "industry-auditable, whole-program certification" is material. That gap is where the claim "SPARK is still the practical option for whole-program certifiable verification today" rests.

A few clarifications that may help collapse confusion in the thread:

  - When I say SPARK provides "industrial-strength, auditable" verification I mean the whole artifact chain: language contracts or annotations, a prover that produces verification conditions and discharge evidence, and vendor/supplier materials practitioners can use in DO-178C / EN-50128 / ISO 26262 certification efforts. That is different from saying "SPARK can verify X and Rust cannot verify X in any research setting".

  - When you observe that SPARK originally used annotations/comments and later adopted Ada 2012 syntax, that is historically correct and expected. The fact that the syntax later became native to Ada strengthens the point that Ada and SPARK are conceptually aligned, not orthogonal.

  - When you say "nothing prevents Rust from gaining a formal spec or evolving toward verification", that is also true; there are active efforts in that direction. The question I keep returning to is: how much engineering, process, and qualification effort is required before Rust + tools equals SPARK's current production story? My answer is: a lot. May not be impossible, but it is definitely not trivial, and not the same as "Rust already provides that".

TL;DR:

The relevant point remains that Ada+SPARK are an integrated, production-ready verification ecosystem today, whereas Rust is a promising base for verification research that has not yet produced the same integrated, certifiable toolchain."

---

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

Ada 83 Rationale: it explains the design goals (reliability, maintainability, suitability for real-time/embedded and defense systems) and the language design decisions (strong typing, modularity, explicitness)[1].

Origin and requirements driving Ada: describes the DoD process (HOLWG / Steelman) that produced a set of requirements targeted at embedded, safety-critical systems and explains why a new language (Ada) was commissioned. It shows Ada was created to serve DoD embedded-system needs.[2]

Standardization process and the language rationale across revisions (shows continuity of safety/verification goals)[3].

Guide for the Use of the Ada Programming Language in High-Integrity / Safety-Critical Systems (technical guidance / conformance): this guide and related validation/ACATS materials describe expectations for Ada compilers and use in safety-critical systems and explain the certification-oriented aspects of Ada toolchains. It is useful to show the ecosystem and qualification emphasis, as per your request.

[1] https://archive.adaic.com/standards/83rat/html/ratl-01-01.ht...

[2] https://archive.adaic.com/pol-hist/history/holwg-93/holwg-93...

[3] https://www.adaic.org/ada-resources/standards/ada-95-documen...

[4] https://www.open-std.org/JTC1/SC22/WG9/n350.pdf

[5] See my other links with regarding to SPARK's history.

[aw1621107]

> You made several good points. I agree with some of them and I think the remainder is a matter of framing. Below is a hopefully direct, precise reply that (a) acknowledges the valid objections, (b) restates the crux of your original argument cleanly, and (c) points the discussion toward the practical/architectural distinction that matters for verification and certification.

...I had my suspicions, and this and the rest of the comment really isn't helping.

> My position is not: "SPARK is merely an older tool and therefore superior".

I don't believe I was claiming that that was your position either?

> My position is:

Most of these points are basically completely tangential to the rest of the thread.

> The fact that the syntax later became native to Ada strengthens the point that Ada and SPARK are conceptually aligned, not orthogonal.

This completely misses the point I was trying to make.

> The question I keep returning to is: how much engineering, process, and qualification effort is required before Rust + tools equals SPARK's current production story?

As does this, because that's certainly not what I was responding to.

> My answer is: a lot. May not be impossible, but it is definitely not trivial

That's absolutely not what you claimed earlier!

> and not the same as "Rust already provides that".

Did anyone claim that in the first place?

> The relevant point remains that Ada+SPARK are an integrated, production-ready verification ecosystem today, whereas Rust is a promising base for verification research that has not yet produced the same integrated, certifiable toolchain."

And for at least a third time, you're comparing SPARK and Rust, which is not an interesting topic of discussion here.

> Ada 83 Rationale: it explains the design goals (reliability, maintainability, suitability for real-time/embedded and defense systems) and the language design decisions (strong typing, modularity, explicitness)[1]. <snip>

I'm not sure this or the rest of the comment is relevant for what I was getting at. I was wondering whether the Ada 83 rationale contained discussion about design elements specifically for validation. Not just things that are usable for validation such as strong types; I'm looking for decisions specifically made with formal validation in mind.

[johnisgood]

> I'm not sure this or the rest of the comment is relevant for what I was getting at. I was wondering whether the Ada 83 rationale contained discussion about design elements specifically for validation. Not just things that are usable for validation such as strong types; I'm looking for decisions specifically made with formal validation in mind.

Quotes to look at from my previous comment:

> Origin and requirements driving Ada: describes the DoD process (HOLWG / Steelman) that produced a set of requirements targeted at embedded, safety-critical systems and explains why a new language (Ada) was commissioned. It shows Ada was created to serve DoD embedded-system needs.[2]

> Standardization process and the language rationale across revisions (shows continuity of safety/verification goals)[3].

> Guide for the Use of the Ada Programming Language in High-Integrity / Safety-Critical Systems (technical guidance / conformance): this guide and related validation/ACATS materials describe expectations for Ada compilers and use in safety-critical systems and explain the certification-oriented aspects of Ada toolchains. It is useful to show the ecosystem and qualification emphasis, as per your request.

Check out the links, specifically [2] and [3]. Find the URLs in previous comment.

[aw1621107]

Again, I'm looking for decisions specifically made with formal verification in mind (e.g., "we made this decision specifically because it would be useful for formal verification"), not just decisions that are usable for validation but whose reasoning did not specifically consider the possibility of formal verification. Barely anything in those quotes even starts to address that, let alone provide any detail on how.

Link [2] does not seem to have any directly relevant bits based on a quick search. There is a short section which seems potentially relevant, but that work was not officially adopted and it's unclear to what extent it influenced Ada 83, especially since some of that work extended through 1987. I'm also not entirely sure how on point it is; unfortunately, it lacks the detail needed for me to tell for sure.

Link [3] is not directly relevant since it concerns Ada 95, whereas my initial comment was specifically about Ada 83. In addition, it doesn't really say anything on its own; it's basically an index of other documents, and I'm not currently well-equipped to go trawling through them for relevant quotes.

The last paragraph is not relevant because I'm looking for information on design decisions. A guide on how to use a language covers a very different subject matter.

I'm not even sure why I am the one doing the digging, really...

[johnisgood]

Are we really getting the same results for these links?

For example in the last one, search for "The Choice of Language".

You will find similar writings in the others.

[aw1621107]

> For example in the last one, search for "The Choice of Language".

That section is non-responsive to what I was wondering about. Once again, I'm looking for decisions made during Ada's creation that were made specifically with formal verification in mind. The section with that title does not discuss that since it's not about Ada's design process at all. The document's date (98-08-17) is another hint that it is not likely to be relevant.

> You will find similar writings in the others.

Would you mind quoting them? I was not able to find relevant passages in the places I looked.