<div>On Mon, 13 Jul 2020 at 19:29, <<a href="mailto:andrew@andrewbanks.com">andrew@andrewbanks.com</a>> wrote:<br></div><div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;padding-left:1ex;border-left-color:rgb(204,204,204)">
But surely, at some stage, "Correctness" can only be actually proven by <br>
EXECUTING that code on the target hardware.<br>
<br>
There are nuances and subtleties that can only ever be truly discovered <br>
by running the code it its true environment.</blockquote><div dir="auto"><br></div><div dir="auto">As far as I know, the proponents of “Correctness by Construction” have never claimed that testing has no role to play in software verification. Rather, it is their contention that other techniques, including formal methods but also including methods such as critical inspection of one’s own code, are more efficient and more effective in demonstrating certain properties of the software.</div><div dir="auto"><br></div><div dir="auto">I’m reminded of an anecdote in the “The Machine That Changed The World”, the book about lean production. At the time the book was written (1991), the only difference between the Volkswagen production line and the Mercedes-Benz production line was that Mercedes-Benz employed technicians to check each car that came off the production line and fix any defects found. That was why Mercedes-Benz cars were higher quality, but also more expensive, than Volkswagens. On the other hand, Toyota stopped the production line as soon as any component was found to be out of tolerance. They carried out root-cause analysis so as to eliminate the defect at source. Toyota claimed that the production line soon settled down to produce cars in which every component worked as intended, meaning they could manufacture cars with the quality of a Mercedes-Benz for the price of a Volkswagen,</div><div dir="auto"><br></div><div dir="auto">Yours,</div><div dir="auto">Dewi</div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;padding-left:1ex;border-left-color:rgb(204,204,204)"></blockquote></div></div>-- <br><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><p><a name="SignatureSanitizer_SafeHtmlFilter_UNIQUE_ID_SafeHtmlFilter__MailAutoSig"><span style="font-size:10pt;font-family:Arial,sans-serif">Yours,</span></a></p><p><span style="font-family:Arial,sans-serif;font-size:10pt">Dewi Daniels | Director | Software Safety Limited</span><br></p><p><span lang="FR" style="font-size:10pt;font-family:Arial,sans-serif">Telephone +44 7968 837742 | Email </span><span lang="FR" style="font-size:10pt;font-family:Arial,sans-serif;color:purple"><a href="mailto:ddaniels@verocel.com" target="_blank">d</a><a href="mailto:ewi.daniels@software-safety.com" target="_blank">ewi.daniels@software-safety.com</a></span></p><p><font face="Arial, sans-serif">Software Safety Limited is a company registered in England and Wales. Company number: </font><font face="Arial, sans-serif">9390590</font><font face="Arial, sans-serif">. Registered office: Fairfield, 30F Bratton Road, West Ashton, Trowbridge</font><span style="font-size:small;font-family:Arial,sans-serif">, United Kingdom </span><span style="font-size:small;font-family:Arial,sans-serif">BA14 6AZ</span></p></div></div>