[SystemSafety] 7% of mistakes in Coq proofs go undetected

[Derek M Jones]

Michael,

> What is 'robustness', please?

Writing code in a way such that any mistakes are either easily
detected (by the compiler or during review).

For instance, making use of strong typing.  It is possible to write
code in a language that supports strong typing, without making used
of the functionality provided.

https://shape-of-code.coding-guidelines.com/2014/08/27/evidence-for-the-benefits-of-strong-typing-where-is-it/

> -- Michael Jackson
> 
>> On 9 Dec 2019, at 12:03, Derek M Jones <derek at knosof.co.uk> wrote:
>>
>> I wish software engineering had something to teach about structuring
>> code for robustness.  There is little evidence that anything works.
>> This is mainly due to the lack of experiments, rather than experiments
>> showing negative results.
>>
>> -- 
>> Derek M. Jones           Software analysis
>> tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com
>> _______________________________________________
>> 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