Re: Interesting article on ARG work

["Dan'l Miller" <optikos@verizon.net>]

On Wednesday, April 4, 2018 at 10:30:04 AM UTC-5, gerdien....@gmail.com wrote:
> http://www.dtic.mil/docs/citations/ADA177802
> A W-Grammar Description for ADA.
> 
> enjoy.

Nice!

“More study is needed in the area of formal expression for semantics-especially in the area of an expression medium. W-grammars may prove too cumbersome for use in situations where the individual grammatical symbols must be manipulated. This thesis proves the possibility of describing Ada's static semantics formally, but some other method such as axiomatic definition might produce a more useful form for such uses as formal correctness proofs.”
—page 43 therein

I'd agree with that wholeheartedly.  Roy Flowers's “axiomatic” therein ≈ my “symbolic logic” above.

Randy, if you really want to make Ada bullet-proof for safety-critical systems, then the ARM as English prose needs to eventually be retired (e.g., for the next revision of Ada post-Ada2020), replaced by something like a MetaAda based on axioms and deductive logic thereof with something analogous to SPARK (or Ocaml's Coq) finding all the illogicalness and lack of covered cases.  (Bojan's lack of named pragma-asserts would be perhaps the very least among the thousand conflicts & gaps & wrinkles & dohs! that such analysis would find.)  And the first A of the AARM would still exist in a different format as why-commentary on the axioms & their logical deductions.  Indeed, there might be a generated English-prose dump of the MetaAda axioms & logical deductions, where the ARM-as-prose would no longer be human-authored and the AARM would be the generated-ARM dump but including the ARG's why-comments throughout the MetaAda symbolic-logic code.

Right now, the ARG mailing list's content as well as some of the deep technically-insightful content of comp.lang.ada's English prose are effectively a mechanical-Turk precursor of the SPARK-esque/Coq-esque thingy that would grind on the axioms and logical deductions in Ada2025's MetaAda ARM-replacement.