Although the CompCert paper explicitly says that the parsing step, as well as the assembling/linking steps, are not verified, this kind of bug is a huge blow to the credibility of formal methods. It really makes you wonder what sort of bugs formal verification is supposed to catch.
That's strange I reach the exact opposite conclusion on this statement.
Author here. I guess what I was trying to say is that CompCert as a system has been trusted for over 10 years, yet only now do we find such a silly correctness bug. People won't read the paper to find out that parsing is unverified, they'll just trust CompCert because they hear it's been rubber-stamped as "formally verified". And that's dangerous.
A better way to do it is pull up C compilers, get their bug rates, and compare it to CompCert for both unverified and verified parts. First tests formal specs + safe language where latter tests verification. You can use smaller, C compilers if uou want to be fair. Two or three spec errors versus what you find in other compilers would corroborate CompCert team's claims. Likewise for verified TLS versus ad hoc protocols or implementations.
That's strange I reach the exact opposite conclusion on this statement.