4 ms·
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
by ghostly_gray 9y ago
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.
- nickpsecurity 9y agoA 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.