[SystemSafety] Number Theorist Fears All Published Math Is Wrong

[David MENTRÉ]

Dear Mr Jones,

Le 09/12/2019 à 15:38, Derek M Jones a écrit :
>> "The second contribution is a *soundness proof* for this algorithm,
>> mechanized using
>> the Coq proof assistant, guaranteeing with the highest confidence that
>> if the
>> validation of an automaton A against a grammar G succeeds, then the
>> automa-
>> ton A and the interpreter that executes it form a *correct* parser for
>> G." (p. 2 of the paper, bold is mine)
>
> There is no proof that the grammar G has any connection to C, or
> any other language.

Of course. The grammar G is the specification, we go back to other
discussion thread, where I said the specification should be checked
through other means.

In the case of CompCert certification for Airbus, an interpreter was
built using the grammar and its associated formal semantics, and this
interpreter was thoroughly tested. If I remember correctly discussion
with one researcher behind CompCert, 4 bugs were found. All in the dark
corners of the C language semantics.

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?

Best regards,
D. Mentré


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