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 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!feeder.erje.net!1.eu.feeder.erje.net!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail From: Niklas Holsti Newsgroups: comp.lang.ada Subject: Re: Ada Successor Language Date: Wed, 6 Jun 2018 12:13:22 +0300 Organization: Tidorum Ltd Message-ID: References: <5e86db65-84b9-4b5b-9aea-427a658b5ae7@googlegroups.com> <878t7u1cfm.fsf@nightsong.com> Mime-Version: 1.0 Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: 7bit X-Trace: individual.net WB5itHhaUJzN1ji2UCpxxAyNDO3AN+ubsNKh6ZaT44JjeRsyaq Cancel-Lock: sha1:qk4OHQrw6TVg0I9mLqxBEsFp5bM= User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:45.0) Gecko/20100101 Thunderbird/45.8.0 In-Reply-To: <878t7u1cfm.fsf@nightsong.com> Xref: reader02.eternal-september.org comp.lang.ada:52952 Date: 2018-06-06T12:13:22+03:00 List-Id: On 18-06-05 00:14 , Paul Rubin wrote: > Shark8 writes: >> (1) The Meta language >> (2) The Generic Language >> (3) The Concurrent/Parallelism language >> (4) The Proving language [SPARK] >> (5) The HW/Representation language > > By "Meta language" I first thought you meant replacing the ARM with a > machine checkable specification, written in something like Twelf[1]. > That seems like a great idea. I agree strongly. Extending the ARM with a formal specification would, I believe, make it much easier to evolve Ada further, assuming that the formalization would permit automatic analysis and proof of properties of the language, such as the absence of Beaujolais effects and the absence of contradictory specifications in different parts of the ARM. This would make it easier to understand the impact of any proposed change to Ada, both for backward compatibility and for the properties of the changed language. It might make it easier to permit language changes that break backward compatibility: by showing precisely where and how that break affects the language, it might help compilers optionally support both the old and the new forms of the language. The formalization should allow the automatic generation of an Ada parser and semantic analyzer, to the same level as ASIS now provides. Such a tool, even if not fast enough for a production compiler, should mitigate the obstacles that the rich (some would say "complex") Ada syntax and semantics now pose for experimental language extensions and language "augmentation" tools (source-to-source tools). This formalization will not be easy or cheap, but should be feasible today, at least for the syntax and static semantics. I'm not sure if the dynamic semantics can be formalized in a way that permits proof of its properties (as opposed to mere simulation of the execution). The increasing powers of program-proving tools make me hopeful. However, current tools focus on proving properties of a particular (single) program, but proving properties of the Ada dynamic semantics would require considering all Ada programs that obey those semantics. Note that I do not insist on a formalization that provides fully automatic proofs, just one that allows formal (automatically checked) proofs, even if manually guided or programmed. To comment on the general "Ada successor" discussion, I think the language should be kept integrated, for example with the "Proving language" being an integrated part of the whole, as in Ada 2012 contracts, rather than being an add-on, as with the original SPARK embedded in Ada comments. -- Niklas Holsti Tidorum Ltd niklas holsti tidorum fi . @ .