Re: Ada Successor Language

[Niklas Holsti <niklas.holsti@tidorum.invalid>]

On 18-06-05 00:14 , Paul Rubin wrote:
> Shark8 <onewingedshark@gmail.com> 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
       .      @       .