[SystemSafety] Number Theorist Fears All Published Math Is Wrong

[Roderick Chapman]

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


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