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