From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 10.107.175.131 with SMTP id p3mr8624604ioo.31.1522858151255; Wed, 04 Apr 2018 09:09:11 -0700 (PDT) X-Received: by 2002:a9d:730a:: with SMTP id e10-v6mr1057729otk.8.1522858150962; Wed, 04 Apr 2018 09:09:10 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!news.unit0.net!peer03.am4!peer.am4.highwinds-media.com!peer02.iad!feed-me.highwinds-media.com!news.highwinds-media.com!u184-v6no6425854ita.0!news-out.google.com!u64-v6ni8047itb.0!nntp.google.com!u184-v6no6425847ita.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Wed, 4 Apr 2018 09:09:10 -0700 (PDT) In-Reply-To: <2c18d429-5b5a-4472-af3d-aedd3ae6a34a@googlegroups.com> Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=47.185.233.194; posting-account=zwxLlwoAAAChLBU7oraRzNDnqQYkYbpo NNTP-Posting-Host: 47.185.233.194 References: <1b44444f-c1b3-414e-84fb-8798961487c3@googlegroups.com> <62ee0aac-49da-4925-b9aa-a16695b3fc45@googlegroups.com> <9879872e-c18a-4667-afe5-41ce0f54559f@googlegroups.com> <2c18d429-5b5a-4472-af3d-aedd3ae6a34a@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <93badc1a-6317-4b6c-b917-92e24d2abab2@googlegroups.com> Subject: Re: Interesting article on ARG work From: "Dan'l Miller" Injection-Date: Wed, 04 Apr 2018 16:09:11 +0000 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Received-Bytes: 3583 X-Received-Body-CRC: 1739990211 Xref: reader02.eternal-september.org comp.lang.ada:51333 Date: 2018-04-04T09:09:10-07:00 List-Id: On Wednesday, April 4, 2018 at 10:30:04 AM UTC-5, gerdien....@gmail.com wro= te: > http://www.dtic.mil/docs/citations/ADA177802 > A W-Grammar Description for ADA. >=20 > enjoy. Nice! =E2=80=9CMore study is needed in the area of formal expression for semantic= s-especially in the area of an expression medium. W-grammars may prove too = cumbersome for use in situations where the individual grammatical symbols m= ust be manipulated. This thesis proves the possibility of describing Ada's = static semantics formally, but some other method such as axiomatic definiti= on might produce a more useful form for such uses as formal correctness pro= ofs.=E2=80=9D =E2=80=94page 43 therein I'd agree with that wholeheartedly. Roy Flowers's =E2=80=9Caxiomatic=E2=80= =9D therein =E2=89=88 my =E2=80=9Csymbolic logic=E2=80=9D above. Randy, if you really want to make Ada bullet-proof for safety-critical syst= ems, then the ARM as English prose needs to eventually be retired (e.g., fo= r the next revision of Ada post-Ada2020), replaced by something like a Meta= Ada based on axioms and deductive logic thereof with something analogous to= SPARK (or Ocaml's Coq) finding all the illogicalness and lack of covered c= ases. (Bojan's lack of named pragma-asserts would be perhaps the very leas= t 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 & log= ical deductions, where the ARM-as-prose would no longer be human-authored a= nd the AARM would be the generated-ARM dump but including the ARG's why-com= ments throughout the MetaAda symbolic-logic code. Right now, the ARG mailing list's content as well as some of the deep techn= ically-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-replace= ment.