comp.lang.ada
 help / color / mirror / Atom feed
From: "G.B." <bauhaus@futureapps.invalid>
Subject: Re: Languages don't  matter.  A mathematical refutation
Date: Thu, 09 Apr 2015 17:43:46 +0200
Date: 2015-04-09T17:43:46+02:00	[thread overview]
Message-ID: <mg66lo$dju$1@dont-email.me> (raw)
In-Reply-To: <s6qwug7m3ywv.1texos0ylbq3s.dlg@40tude.net>

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.

  reply	other threads:[~2015-04-09 15:43 UTC|newest]

Thread overview: 94+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2015-03-25 11:46 Languages don't matter. A mathematical refutation Jean François Martinez
2015-03-25 15:19 ` Paul Rubin
2015-04-03  0:50   ` robin.vowels
2015-04-03  2:18     ` Jeffrey Carter
2015-04-03 13:37       ` Bob Duff
2015-04-03 14:13         ` Dmitry A. Kazakov
2015-04-03 17:34           ` Paul Rubin
2015-04-03 19:34             ` Dmitry A. Kazakov
2015-04-03 19:58               ` Paul Rubin
2015-04-04  6:59                 ` Dmitry A. Kazakov
2015-04-06 21:12                   ` Paul Rubin
2015-04-07  5:57                     ` Dmitry A. Kazakov
2015-04-08  4:12                       ` Paul Rubin
2015-04-08  6:45                         ` Dmitry A. Kazakov
2015-04-04  0:41             ` Dennis Lee Bieber
2015-04-04  3:05               ` Paul Rubin
2015-04-04 14:46                 ` Dennis Lee Bieber
2015-04-04 15:41                   ` brbarkstrom
2015-04-04 19:20                   ` Paul Rubin
2015-04-04 20:00                     ` Dmitry A. Kazakov
2015-04-04 20:44                       ` Paul Rubin
2015-04-05  8:00                         ` Dmitry A. Kazakov
2015-04-05  9:55                           ` Brian Drummond
2015-04-06 21:27                             ` Randy Brukardt
2015-04-06 17:07                           ` Paul Rubin
2015-04-06 17:41                             ` Dmitry A. Kazakov
2015-04-06 18:35                               ` Paul Rubin
2015-04-06 21:46                                 ` Randy Brukardt
2015-04-06 22:12                                   ` Paul Rubin
2015-04-06 23:40                                     ` Jeffrey Carter
2015-04-07 19:07                                     ` Randy Brukardt
2015-04-08  3:53                                       ` Paul Rubin
2015-04-08 21:16                                         ` Randy Brukardt
2015-04-09  1:36                                           ` Paul Rubin
2015-04-09 23:26                                             ` Randy Brukardt
2015-04-09  2:36                                           ` David Botton
2015-04-09  8:55                                           ` Georg Bauhaus
2015-04-09  9:38                                             ` Dmitry A. Kazakov
2015-04-09 13:14                                               ` G.B.
2015-04-09 14:35                                                 ` Dmitry A. Kazakov
2015-04-09 15:43                                                   ` G.B. [this message]
2015-04-09 17:26                                                     ` Dmitry A. Kazakov
2015-04-09 18:40                                                   ` Niklas Holsti
2015-04-09 19:02                                                     ` Dmitry A. Kazakov
2015-04-09 20:38                                                       ` Paul Rubin
2015-04-09 23:35                                             ` Randy Brukardt
2015-04-10 14:16                                               ` G.B.
2015-04-10 20:58                                                 ` Randy Brukardt
2015-04-07  0:36                                 ` Dennis Lee Bieber
2015-04-05 13:57                     ` Dennis Lee Bieber
2015-04-03 16:17         ` J-P. Rosen
2015-04-03 17:33           ` Bob Duff
2015-04-26 11:38             ` David Thompson
2015-04-03 19:00         ` Georg Bauhaus
2015-04-03 19:12         ` Jeffrey Carter
2015-04-03 22:37           ` Bob Duff
2015-04-03 23:38             ` Jeffrey Carter
2015-04-04  0:15               ` Bob Duff
2015-04-04  7:06                 ` Dmitry A. Kazakov
2015-04-04  2:59               ` Paul Rubin
2015-04-04  0:56             ` Dennis Lee Bieber
2015-03-25 17:12 ` Jean François Martinez
2015-03-26 13:43 ` Maciej Sobczak
2015-03-26 15:01   ` Jean François Martinez
2015-03-26 17:45     ` Jeffrey Carter
2015-03-26 15:21   ` Dmitry A. Kazakov
2015-03-27 11:25     ` Jean François Martinez
2015-03-27 17:36       ` Dmitry A. Kazakov
2015-03-30 10:31         ` Jean François Martinez
2015-03-30 11:52           ` Dmitry A. Kazakov
2015-03-30 12:32             ` G.B.
2015-03-30 13:48               ` Dmitry A. Kazakov
2015-03-30 15:47                 ` G.B.
2015-03-30 16:05                   ` Dmitry A. Kazakov
2015-04-02 12:59                     ` brbarkstrom
2015-04-02 13:35                       ` Dmitry A. Kazakov
2015-04-02 14:48                         ` jm.tarrasa
2015-04-02 15:55                           ` brbarkstrom
2015-04-02 16:21                             ` Jean François Martinez
2015-04-02 16:48                             ` Dmitry A. Kazakov
2015-04-02 16:41                           ` Dmitry A. Kazakov
2015-04-04 10:02                             ` jm.tarrasa
2015-04-04 11:16                               ` Dmitry A. Kazakov
2015-04-02 15:58                         ` Jean François Martinez
2015-04-02 16:39                           ` Dmitry A. Kazakov
2015-04-03  9:46                             ` Jean François Martinez
2015-04-03 14:00                               ` Dmitry A. Kazakov
2015-04-03 17:12                                 ` Jean François Martinez
2015-04-02 17:17                         ` G.B.
2015-04-02 19:09                           ` Dmitry A. Kazakov
2015-04-02 18:24                       ` Niklas Holsti
2015-04-02 18:43                       ` Jeffrey Carter
2015-03-30 11:36         ` Jean François Martinez
2015-03-30 10:48       ` jm.tarrasa
replies disabled

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox