[SystemSafety] Number Theorist Fears All Published Math Is Wrong

[Derek M Jones]

Martyn,

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

Exactly, what are the cost benefits.

> 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)   ?

There are tools that do particular tasks more cost effectively than
other tools.

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

I am not proposing that writing test cases is the only technique
that should be used.

The more mathematical approaches can do some tasks more cost effectively
than writing test cases.

None of the available techniques proves correctness of the software.
They all operate by showing an absence of (presumably undesirable)
behavior.


> 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.
>>
>>
> 
> 
> 
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
> 

-- 
Derek M. Jones           Software analysis
tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com