Re: Languages don't matter. A mathematical refutation

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Thu, 09 Apr 2015 17:43:46 +0200, G.B. wrote:

> 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))"

How are you going to compute this? Not to mention that is does not depend
on what the subprogram actually does, on its code. Let you take two CPUs
running it. One is circling a neutron star. Which one fulfils the contract
and according to which clock?

>>> 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?

So might be power consumption, weight, emitted radiation etc. None of which
is functional.

>>> 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.

The contract you cannot state.

>>> 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?

"Why" and "else" applied to what?

>> 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.

gotos are absolutely well-behaved = as defined in the RM. Which changes
nothing. You are confusing language with the program (not for the first
time).

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de