From: Paul Rubin <no.email@nospam.invalid>
Subject: Re: Languages don't matter. A mathematical refutation
Date: Thu, 09 Apr 2015 13:38:03 -0700
Date: 2015-04-09T13:38:03-07:00 [thread overview]
Message-ID: <87bnixdolw.fsf@jester.gateway.sonic.net> (raw)
In-Reply-To: 1pjgcrsn42a55.b9xlyrybsns1$.dlg@40tude.net
"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> And "will take" is not "took". Furthermore, it is not a proper
> contract anyway, as it cannot be verified *before* a program run. The
> [proper] contract must apply to all possible runs (all program
> states).
As G.B. explained, the contract is simply:
"... if #slots >= N/M, then
for all x . TIME(x, Table, Find) <= f(M, N, g(Hash))"
That contract has a quantifier ("for all x") but that's not inherently
an obstacle to static verification, given a precise enough semantics for
the implementation language that the TIME function can be computed.
It's just like any other mathematical theorem, e.g.
if integer n > 2, then
for all integers a,b,c > 0, a**n + b**n /= c**n
Proof of this theorem is left as an exercise ;-)
The point is that verifying the contract means proving a certain
sentence in predicate logic. It's likely to be messy in practice, but
conceptually it's straightforward. We know how to build proof systems
that deal with quantifiers.
next prev parent reply other threads:[~2015-04-09 20:38 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.
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 [this message]
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