<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>