Re: Seeking for papers about tagged types vs access to subprograms

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

On 10.05.13 16:27, Dmitry A. Kazakov wrote:
> On Fri, 10 May 2013 16:01:46 +0200, Yannick Duchêne (Hibou57) wrote:
>
>> Le Fri, 10 May 2013 15:54:40 +0200, Dmitry A. Kazakov
>> <mailbox@dmitry-kazakov.de> a écrit:
>>>>> Human intervention is needed to handle the semantics, not because of
>>>>> multiplicity of implementations. You could choose them randomly.
>>>>
>>>> You can't choose randomly, the program must have runtime properties as
>>>> well.
>>>
>>> The only properties a program must have are derived from its semantics,
>>> per definition.
>>
>> The time required for a computation, the memory used, are not part of the
>> semantic.
>
> It is for RT or else irrelevant.

"It" becomes a compile time thing as soon as we can state meaningfully
(hence, checked by the compiler), in source text, that some part of a
program must (and will) make bounded use of resources, where "bounded"
is not trivially true but specifically true of the program being
translated.

Semi-formally, the data structure parts of C++ and Ada have made a
move in this direction by advising that certain language-provided
operations on containers be bounded specifically.

It will be sufficient if compilers decide this when translating the
very few (compared to the possible) of the non-undecidable programs
that warrant our profession.