[SystemSafety] Number Theorist Fears All Published Math Is Wrong

David MENTRÉ David.MENTRE at bentobako.org
Wed Dec 11 08:30:15 CET 2019


Dear Mr Jones,

Le 09/12/2019 à 21:38, Derek M Jones a écrit :
>> By the way, how do you know that the grammar of C used in gcc, Clang,
>> diab or any other C compiler is the correct one?
>
> These compiler vendors don't make any claims that their compilers have
> been proved correct.

Yes. But nonetheless those buggy compilers are used to make safety
critical systems, at the expense of users of those systems.

You can say whatever you want about the "soap power advertising" of
formal methods, but nonetheless I have much more trust in CompCert that
any other traditional compiler. And this trust is not built on mailing
list discussion, but on scientific facts found in peer-reviewed literature. 

Best regards,
D. Mentré


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20191211/13f7497b/attachment.html>


More information about the systemsafety mailing list