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=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 border2.nntp.dca1.giganews.com!nntp.giganews.com!usenet.blueworldhosting.com!feeder01.blueworldhosting.com!feeder.erje.net!eu.feeder.erje.net!newsfeed.fsmpi.rwth-aachen.de!newsfeed.straub-nv.de!eternal-september.org!feeder.eternal-september.org!mx02.eternal-september.org!.POSTED!not-for-mail
From: Paul Rubin <no.email@nospam.invalid>
Newsgroups: comp.lang.ada
Subject: Re: Languages don't  matter.  A mathematical refutation
Date: Thu, 09 Apr 2015 13:38:03 -0700
Organization: A noiseless patient Spider
Message-ID: <87bnixdolw.fsf@jester.gateway.sonic.net>
References: <b3592526-729a-4198-a630-696542b3f3be@googlegroups.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>
 <convbvF6ra0U1@mid.individual.net>
 <1pjgcrsn42a55.b9xlyrybsns1$.dlg@40tude.net>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: mx02.eternal-september.org;
 posting-host="bda44be170c76b3ef6d23fecd204a8fa";
 logging-data="22772"; mail-complaints-to="abuse@eternal-september.org";
 posting-account="U2FsdGVkX18Q7WluIGV13EpYFb9HTU92"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3 (gnu/linux)
Cancel-Lock: sha1:WrxfVGeX2PhyRIW8DdS7a5FVIrI=
 sha1:ewsF1W8YWk3L1iMUCbuvL2b0mHc=
Xref: number.nntp.giganews.com comp.lang.ada:192805
Date: 2015-04-09T13:38:03-07:00
List-Id: <comp.lang.ada>

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