[SystemSafety] Number Theorist Fears All Published Math Is Wrong

Derek M Jones derek at knosof.co.uk
Mon Dec 9 21:38:25 CET 2019


David,

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

Did you ask this researcher if they were embarrassed about the
soap powder advertising claims being made about CompCert?

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

-- 
Derek M. Jones           Software analysis
tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com


More information about the systemsafety mailing list