4 ms·

Proving code correct is orders of magnitude harder than the rest IMHO. It is amazing that enough progress has been made that large scale projects like CompCert

Proving code correct is orders of magnitude harder than the rest IMHO. It is amazing that enough progress has been made that large scale projects like CompCert and seL4 can now be done successfully by small teams of people.

Mimmy 4y ago
Interesting... I didn't realize there were large open projects that were formally verified. Are there other examples besides CompCert and seL4?
- mbrodersen 4y ago
  Formally Proven Binary Format Parsers: https://www.microsoft.com/en-us/research/publication/hardening-attack-surfaces-with-formally-proven-binary-format-parsers/ https://www.microsoft.com/en-us/research/publication/hardeni...
- buescher 4y ago
  I don’t know if you’d count it as large, but portions of Amazon FreeRTOS.
Beltiras 4y ago
I'd say it is not hard but impossible. I have a hard enough time to get requirements specifications that are unambiguous. Proving I coded what I was asked for is not a rigorous science practice. It's a social contract.
- dahfizz 4y ago
  That's a software engineering problem, not a computer science one.
- AnimalMuppet 4y ago
  I agree with "impossible". In fact, it's worse than you say. Specs can be unambiguous and still be wrong. How do you prove that the specification doesn't have a bug? And then, you can formally prove that code does not have certain kinds of bugs. You cannot formally prove that code has no bugs, because 1) you don't even know all possible kinds of bugs, and 2) even for the kinds you do know, you don't have formal proofs for all of them.
  - Beltiras 4y ago
    Bugs in the specs. Yum.
- mbrodersen 4y ago
  No bugs have ever been found in CompCert and seL4. The NSA gave up trying to hack seL4. The first time that has ever happened. So yes there might in theory still be bugs in the specs for CompCert and seL4. However the results speak for themselves.
- mbrodersen 4y ago
  Non-proven correct software doesn’t even have formal specs. Having a formal spec is already light years ahead of other software because it forces you to nail down exactly what the code is supposed to do.

Mimmy 4y ago

Interesting... I didn't realize there were large open projects that were formally verified. Are there other examples besides CompCert and seL4?

mbrodersen 4y ago
Formally Proven Binary Format Parsers: https://www.microsoft.com/en-us/research/publication/hardening-attack-surfaces-with-formally-proven-binary-format-parsers/ https://www.microsoft.com/en-us/research/publication/hardeni...
buescher 4y ago
I don’t know if you’d count it as large, but portions of Amazon FreeRTOS.

Beltiras 4y ago

I'd say it is not hard but impossible. I have a hard enough time to get requirements specifications that are unambiguous. Proving I coded what I was asked for is not a rigorous science practice. It's a social contract.

dahfizz 4y ago
That's a software engineering problem, not a computer science one.
AnimalMuppet 4y ago
I agree with "impossible". In fact, it's worse than you say. Specs can be unambiguous and still be wrong. How do you prove that the specification doesn't have a bug? And then, you can formally prove that code does not have certain kinds of bugs. You cannot formally prove that code has no bugs, because 1) you don't even know all possible kinds of bugs, and 2) even for the kinds you do know, you don't have formal proofs for all of them.
- Beltiras 4y ago
  Bugs in the specs. Yum.
mbrodersen 4y ago
No bugs have ever been found in CompCert and seL4. The NSA gave up trying to hack seL4. The first time that has ever happened. So yes there might in theory still be bugs in the specs for CompCert and seL4. However the results speak for themselves.
mbrodersen 4y ago
Non-proven correct software doesn’t even have formal specs. Having a formal spec is already light years ahead of other software because it forces you to nail down exactly what the code is supposed to do.