[SystemSafety] Number Theorist Fears All Published Math Is Wrong

[Peter Bernard Ladkin]

On 2019-10-31 20:53 , Derek M Jones wrote:
> 
> Claiming to have verified a compiler, when in fact the work only
> applies to parts of the code generator, is soap powder advertising.

Yes, but who does this for usable products?

Almost all brief claims are backed up in depth, because anyone who might want to use such a compiler
likely will have to deal with inspectors and regulators who will not be satisfied with a simple
statement "We used Company X's compiler which is formally verified" but will want to see appropriate
V&V.

For example, Ansys says SCADE is "certified to IEC 61508:2010 SIL 3". Even though IEC 61508 makes no
provision for certification, TÜV Süd has indeed certified it. TÜV Süd/Ansys is happy to tell you
exactly what that means, namely that there is a certificate on TÜV Süd's letterhead and a detailed
document available to users explaining exactly what has been verified/validated by TÜV Süd's
inspection. (Of course, some of it may be hard to fathom, but that is surely to be expected; there
is no simple recipe book for using sophisticated SW development tools.)

Similarly, AbsInt says "CompCert is a formally verified optimizing C com­piler for safety-critical
and mission-critical soft­ware" and Daniel Kästner has discussed with me in some detail what this
means. They have a considerable amount of backing material including tools to help with any use of
CompCert in the context of DO-178C, IEC 61508 and industry-specific standards.

I'd love to see soap-powder manufacturers take a similar approach to their products. Not that I use
soap powder.

PBL

Prof. Peter Bernard Ladkin, Bielefeld, Germany
MoreInCommon
Je suis Charlie
Tel+msg +49 (0)521 880 7319  www.rvs-bi.de





-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 488 bytes
Desc: OpenPGP digital signature
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20191101/ec18581c/attachment-0001.sig>