4 ms·
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 i
by 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 agoThat's a software engineering problem, not a computer science one.
- AnimalMuppet 4y agoI 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 agoBugs in the specs. Yum.
- mbrodersen 4y agoNo 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 agoNon-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.