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