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=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,39579ad87542da0e
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,UTF8
X-Received: by 10.66.163.8 with SMTP id ye8mr3713687pab.23.1368256932270;
        Sat, 11 May 2013 00:22:12 -0700 (PDT)
Path: 
 ln4ni1876pbb.0!nntp.google.com!news.glorb.com!feeder.erje.net!us.feeder.erje.net!newsfeed.fsmpi.rwth-aachen.de!npeer.de.kpn-eurorings.net!npeer-ng0.de.kpn-eurorings.net!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail
Date: Sat, 11 May 2013 09:22:26 +0200
From: Georg Bauhaus <rm.dash-bauhaus@futureapps.de>
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.7;
 rv:17.0) Gecko/20130328 Thunderbird/17.0.5
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: Seeking for papers about tagged types vs access to subprograms
References: <op.wv8jh1c1ule2fv@cardamome> <op.wwn4oak8ule2fv@cardamome>
 <19lrzzbgm77v6.1dzpgqckptaj6.dlg@40tude.net> <kmbohm$elb$1@loke.gir.dk>
 <p0pf97g5w6xg.jhca6ztjwpde$.dlg@40tude.net> <op.wwq9s4l6ule2fv@cardamome>
 <1bfhq7jo34xpi.p8n2vq6yjsea.dlg@40tude.net> <op.wwrefx1pule2fv@cardamome>
 <cps71yzogw24$.7ol98fxcaurj$.dlg@40tude.net> <op.wwriky0dule2fv@cardamome>
 <nd22gfeezrwf$.tlj4yyygrwq3$.dlg@40tude.net> <kmecg6$et4$1@loke.gir.dk>
 <12gn9wvv1gwfk.10ikfju4rzmnj.dlg@40tude.net> <kmh7d4$up3$1@loke.gir.dk>
 <op.wwumn3r2ule2fv@cardamome> <ebebe368y8s9$.vfm8f23pnkjr.dlg@40tude.net>
 <op.wwu8cmo7ule2fv@cardamome> <1cir6d72wemw.qxx9mozot7hl.dlg@40tude.net>
 <op.wwvb4yczule2fv@cardamome> <ljokf4mmu7eb$.1scqg32yzi4hv.dlg@40tude.net>
 <op.wwvfw8vfule2fv@cardamome> <ql414xt63ugl.1d6nkjnyy90w2.dlg@40tude.net>
In-Reply-To: <ql414xt63ugl.1d6nkjnyy90w2.dlg@40tude.net>
Message-ID: <518df1a3$0$6570$9b4e6d93@newsspool3.arcor-online.net>
Organization: Arcor
NNTP-Posting-Date: 11 May 2013 09:22:11 CEST
NNTP-Posting-Host: 6e5a99d0.newsspool3.arcor-online.net
X-Trace: 
 DXC=cR1cZ6h_?LiPXlQ;h]GTMdMcF=Q^Z^V3h4Fo<]lROoRa8kF<OcfhCOk?4B]c\D1V0jPCY\c7>ejVhWkSnohXh_0`K^PFJSAV[=l
X-Complaints-To: usenet-abuse@arcor.de
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Date: 2013-05-11T09:22:11+02:00
List-Id: <comp.lang.ada>

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.