[SystemSafety] Number Theorist Fears All Published Math Is Wrong

[Martyn Thomas]

All true, of course, and it's important to consider what assumptions you
are making, how confident you are about them and whether you could do
something cost-effective that would improve your confidence. All
engineers have to make some assumptions; the role of formal languages
and tools is to eliminate unnecessary assumptions and ambiguities where
that is possible.

Martyn

On 30/10/2019 10:57, Peter Bishop wrote:
>
> 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.
>
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20191030/cb694276/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 488 bytes
Desc: OpenPGP digital signature
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20191030/cb694276/attachment.sig>