by johnisgood | 2025-10-16 06:36:09+00:00
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.