[SystemSafety] 7% of mistakes in Coq proofs go undetected
Derek M Jones
derek at knosof.co.uk
Mon Dec 9 17:14:26 CET 2019
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
More information about the systemsafety
mailing list