Re: Languages don't matter. A mathematical refutation

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

On Thu, 09 Apr 2015 15:14:59 +0200, G.B. wrote:

> Now, WRT storage management, assume a bounded container.
> The implementation may pre-allocate the maximum number of
> objects.(*) Given that, why should it not be possible at all,
> in no case, to guarantee a known complexity of storage
> management? A bounded vector, say, could specify its
> storage management needs, on condition that ... Much like
> a hash table package would state that
> 
>    "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.

>> GC is non-functional and unrelated to the program behavior, which is
>> another way to explain why GC is neither low nor high level. It is
>> non-existent.
> 
> 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. Any other things happening upon
execution of the program are abstracted away, which is the only way to
define 'behavior' without dragging the whole Universe into the picture.

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

> 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. These are two unrelated things. A correctly behaving GC is still
a bug. Compare it with goto. There is no doubt that jumps and labels behave
correctly...

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