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