[SystemSafety] Number Theorist Fears All Published Math Is Wrong

[Martyn Thomas]

Your "open question" needs more constraints. How confident do you need
to be that your software won't fail?

There are tools that can prove the absence of any fixed-point overflow
in a program. for example, or show you exactly where it could occur. How
long would it take you to do that by testing, in a program that
calculates A, calculates B and then contains the expression 1/(A-B)   ? 
Or to show by testing that your program does not use undefined data, or
violate the bounds of any arrays?

If you can't gain confidence about these small but important properties
by testing the software, what exactly have you discovered by testing it
and carefully checking the results - other than that it runs your test
set correctly (in this particular order, today).

Martyn


On 29/10/2019 16:27, Derek M Jones wrote:
> David,
>
>> Have you every actually used a tool that attempts to provide formal
>> proof of software correctness? If so, how many demonstrably false
>
> "formal proof of software correctness" is a meaningless marketing term.
>
> There are tools that show:
>
>    o for specified input, a specified list of expressions are true,
>
>    o that it was not possible to find any inconsistencies between
> a specification and code claiming to implement the specification.
>
> These tools fail to find faults, just like testing.
>
> The open question is the extent to which they might, or might
> not be more cost effective than testing.
>
>

-------------- 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/20191029/c8a30511/attachment-0001.sig>