<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<div class="moz-cite-prefix">Dear Mr Jones,</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">Le 09/12/2019 à 21:38, Derek M Jones a
écrit :<br>
</div>
<blockquote type="cite"
cite="mid:2a394d88-1ebf-bb7f-2068-f2dbdc668301@knosof.co.uk">
<blockquote type="cite" style="color: #000000;">By the way, how do
you know that the grammar of C used in gcc, Clang,
<br>
diab or any other C compiler is the correct one?
<br>
</blockquote>
<br>
These compiler vendors don't make any claims that their compilers
have
<br>
been proved correct.</blockquote>
<p>Yes. But nonetheless those buggy compilers are used to make
safety critical systems, at the expense of users of those systems.</p>
<p>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. </p>
<p>Best regards,<br>
D. Mentré</p>
<p><br>
</p>
</body>
</html>