[SystemSafety] Number Theorist Fears All Published Math Is Wrong

[Peter Bishop]

I guess the point is that proofs are made in the context of an abstract
machine

So the proof is correct *for the abstract machine*
but only correct in the real world if the implementation preserves
the semantics of the abstract machine.

So to make a claim about real world execution we need to assume
(or prove) the semantics are preserved.

As Rod said, assumptions need to be made about the compiler and
hardware, but there are further gotchas

- there can be resource exhaustion (e.g. the abstract machine has an
infinite stack but the implemented stack is finite).

- the abstract machine has no concept of time, but execution time is an
important property in a real-time context, i.e. a "correct" response
that takes too long is also a defect.

So linking proofs to real world behaviour is always conditional on
factors that lie outside the abstraction used for the proof. 

Peter Bishop
Adelard

On 30/10/2019 09:45, Roderick Chapman wrote:
> On 29/10/2019 18:39, Derek M Jones wrote:
>> I am saying that proofs of correctness don't exist, only evidence that
>> certain kinds of behavior have not been found.
>
> I'd don't think I can agree with that.
>
> In addition to the usual proofs of absence of the most obvious
> defects, I can think of several projects where some non-trivial proofs
> of correctness have been achieved against a formal specification. Most
> of the ones I know of are coded in SPARK, but there are others (e.g.
> Amazon's "s2n" TLS stack and projects using Frama-C).
>
> Of course, these proofs depend on assumptions - that the compiler is
> non-malicious, that the CPU executes the semantics of its ISA
> as-advertised and so on, but I've found those to be both reasonable
> and manageable risks in the past...
>
> Simple example: in SHOLIS, I had to implement a truncating integer
> square root algorithm with the following specification (expressed in
> SPARK 2014 for the purposes of this email):
>
>    subtype Sqrt_Domain is Integer range 0 .. 2**31 - 1;
>    subtype Sqrt_Range  is Integer range 0 .. 46340;
>
>    function Sqrt (X : in Sqrt_Domain) return Sqrt_Range
>      with Post => (Sqrt'Result * Sqrt'Result) <= X and
>                   (Sqrt'Result + 1) * (Sqrt'Result + 1) > X;
>
> Now... there are several ways to implement that - binary chop search,
> Newton-Raphson, Von-Neumann's algorithm etc. etc.  We chose binary
> chop, and proved it correct against that specification. I can post the
> code, VCs and so on if anyone is really interested.
>
> So... why does Derek object to this as a "proof of correctness"?
>
> (An aside: In 1996 (when I wrote that code) we also considered
> Von-Neumann's algorithm, but rejected it because it is rather not
> obvious how it works, and no-one could derive a loop invariant for it
> at the time.  More recently, the team at AdaCore and the Why3 team did
> manage to refine the correct loop invariant and produce a
> semi-automated proof of it - the first mechanized proof of the
> algorithm that I have seen. It's entertaining, and we hope to write it
> up at some point. The algorithm appears in Henry Warren's "Hacker's
> Delight" if you're not familiar with it...)
>
>  - Rod
>
>
>
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety

-- 

Peter Bishop
Chief Scientist
Adelard LLP
24 Waterside, 44-48 Wharf Road, London N1 7UX

Email: pgb at adelard.com
Tel:  +44-(0)20-7832 5850

Registered office: 5th Floor, Ashford Commercial Quarter, 1 Dover Place, Ashford, Kent TN23 1FB
Registered in England & Wales no. OC 304551. VAT no. 454 489808

This e-mail, and any attachments, is confidential and for the use of
the addressee only. If you are not the intended recipient, please
telephone 020 7832 5850. We do not accept legal responsibility for
this e-mail or any viruses.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20191030/cd229974/attachment-0001.html>