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=-0.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!.POSTED!not-for-mail
From: "G.B." <bauhaus@futureapps.invalid>
Newsgroups: comp.lang.ada
Subject: Re: Languages don't  matter.  A mathematical refutation
Date: Thu, 09 Apr 2015 17:43:46 +0200
Organization: A noiseless patient Spider
Message-ID: <mg66lo$dju$1@dont-email.me>
References: <b3592526-729a-4198-a630-696542b3f3be@googlegroups.com>
 <w19y3129v8q1.jkn83uwyte4p$.dlg@40tude.net>
 <87oan56rpn.fsf@jester.gateway.sonic.net>
 <ojcuhapfmqleoec1r4fu7ierr3p85in78r@4ax.com>
 <877fts7fvm.fsf@jester.gateway.sonic.net>
 <cutvhal9n5jobh5ojsof28r9hncdjabbvk@4ax.com>
 <87twwv66pk.fsf@jester.gateway.sonic.net>
 <32ecaopodr1g.1xqh7ssdpa2ud.dlg@40tude.net>
 <87pp7j62ta.fsf@jester.gateway.sonic.net>
 <p6xuoikp37ui$.1ag0rtxnv77c0.dlg@40tude.net>
 <87pp7hb2xo.fsf@jester.gateway.sonic.net>
 <5rxvgyes5xg8.1mqq86gacbsb1.dlg@40tude.net>
 <87lhi5ayuv.fsf@jester.gateway.sonic.net> <mfuusb$pv3$1@loke.gir.dk>
 <87oan0aote.fsf@jester.gateway.sonic.net> <mg19so$rqk$1@loke.gir.dk>
 <878ue3ff6y.fsf@jester.gateway.sonic.net> <mg45qp$tt6$1@loke.gir.dk>
 <mg5eoh$k18$1@dont-email.me> <ajhl78cb3zbg$.1ipt9woml0elc.dlg@40tude.net>
 <mg5tup$bc2$1@dont-email.me> <s6qwug7m3ywv.1texos0ylbq3s.dlg@40tude.net>
Reply-To: nonlegitur@futureapps.de
Mime-Version: 1.0
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Thu, 9 Apr 2015 15:42:48 +0000 (UTC)
Injection-Info: mx02.eternal-september.org;
 posting-host="b96887e80893c84a90c3007226ca0d1c";
	logging-data="13950"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX19GRTb/9j/QAIEfYw+gyWzMZFRLlbIQnWc="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9;
 rv:31.0) Gecko/20100101 Thunderbird/31.6.0
In-Reply-To: <s6qwug7m3ywv.1texos0ylbq3s.dlg@40tude.net>
Cancel-Lock: sha1:x8ynlUa8rzdzoNti8kDBe1JBrR4=
Xref: news.eternal-september.org comp.lang.ada:25492
Date: 2015-04-09T17:43:46+02:00
List-Id: <comp.lang.ada>

On 09.04.15 16:35, Dmitry A. Kazakov wrote:

>>     "As long as the number of slots is as least N/M,
>>      finding an object will take no more than f(M, N, g(Hash))."
>
> Which is elementary incomputable, as it contains the future tense and thus
> cannot be a part of any contract.

"as long as" makes it universal in time. Invariant:

  "... if #slots >= N/M, then
   for all x . TIME(x, Table, Find) <= f(M, N, g(Hash))"


>> Like everything that actually handles program data, GC does
>> influence the program's behavior, e.g. by taking time.
>
> That is not the program behavior. The behavior is only things related to
> the program logic = functional things.

Time is "functionally" essential (milliseconds response time,
say), is not "the universe", but surely is part of observable
behavior?

>> Hence, one may influence GC in server JVMs, for example.
>
> Yes, and this is why GC is a bad idea, since its potentially breaks the
> abstraction and causes unpredicted behavior = *use* of GC is a [potential]
> bug.

Precisely whence a GC contract is required.

>> But that's the point. Suppose there is an abstract description
>> of GC behavior, in terms of parameters. Will the description
>> be sufficiently detailed for guiding the design of an algorithm?
>
> Sure. But that is beside the point. You can design GC and you can do it in
> a fully contractual manner under SPARK with all bells and whistles. But
> that would not change anything for the application program which would try
> to use GC.

Pardon? Why else would you write the contract?

> Compare it with goto. There is no doubt that jumps and labels behave
> correctly...

Which is why Ada adds clauses that make "goto" be (relatively)
well behaved. Like a contract does.