[SystemSafety] Collected stopgap measures (Hoare)

[Derek M Jones]

Nick,

> Who said anything about manual proofs....this was, as I pointed out,
> automatic....

Ok, I had misinterpreted how much was automatic and how much manual.
The 18k over 6-man years looked like primarily a manual proof effort.

The devil is in the detail of what is being proven in a
"proof automation process".

Static analysis tools can check existing source for the presence
of unwanted constructs, with human checks to weed out the false
positives.

The effort needed to check code boils down to the number of
mistakes it contains, how good a job the tool does at not flagging
false positives and the number of different constructs being searched for.

> 
> And BTW, I don't really mind if you believe me or not.
> 
> 
> Nick Tudor
> Tudor Associates Ltd
> Mobile: +44(0)7412 074654
> www.tudorassoc.com
> 
> *77 Barnards Green Road*
> *Malvern*
> *Worcestershire*
> *WR14 3LR*
> *Company No. 07642673*
> *VAT No:116495996*
> 
> *www.aeronautique-associates.com <http://www.aeronautique-associates.com>*
> 
> 
> On Fri, 16 Nov 2018 at 16:03, Derek M Jones <derek at knosof.co.uk> wrote:
> 
>> Nick,
>>
>>> Nope, this is formal proof, and nope, it is not marketing...cheeky!  Use
>> of
>>
>> Four man months to process 350,000 SLoC.
>>
>> Say 20 man days per month, so 80 man days.
>> Which is around 4,500 SLoC per day, for 80 days.
>>
>> Not believable.
>>
>> Now 4-man months to run the tools over something that has already
>> been written and check the results.  That is believable.
>>
>> How long might it have taken to write a proof?
>>
>> If it took 6-man years to write a proof of 18K, then 350K is
>> going to require 100+ man years.
>>
>>
>> --
>> Derek M. Jones           Software analysis
>> tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com
>>
> 

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