4 ms·

Adding the word "formal" to something doesn't mean it can do the impossible. It's not realistic to prove things correct, since it's both an impossible amount of

Adding the word "formal" to something doesn't mean it can do the impossible. It's not realistic to prove things correct, since it's both an impossible amount of work and you'll end up finding that your definition of "correct" was incorrect. (CompCert, a "formally correct C compiler", has had bugs found in it.)

Veserv 3y ago
I do not see how that is relevant to my statement that formal methods, as required by the higher Common Criteria levels, do not constitute “box-ticking exercises”. Or are you arguing that these standards which require proofs of correctness are useless because proofs of correctness are much less impressive than box ticking?
- astrange 3y ago
  They are extremely expensive box ticking exercises. Furthermore, I don't think anything except box ticking exercises exists or could ever exist. You can only write down ways to make a process worse, not better.
  - Veserv 3y ago
    I know that I have more confidence in a proven compiler that is thoroughly tested over a random compiler Joe the intern slammed out, but you do not seem to think that way. That is fine, you do you.
- EVa5I7bHFq9mnYK 3y ago
  Nothing realistically complex can be proven "correct". There is even a mathematical theorem about it - given a program's code, one can't even prove that it ever stops. One can, of course, apply proof of correctness to simple curcuits, where all possible inputs and outputs can be enumerated.
  - Veserv 3y ago
    That is a complete misunderstanding of consequences of Rice’s theorem which generalizes the halting problem. You can not prove non-trivial properties about all programs that could could ever exist with no false positives or false negatives. You can prove non-trivial properties about almost every program. For instance, if I want to disallow programs that will not halt, I can just reject any program with a unbounded loop. I may also reject programs with a unbounded loop that will halt, a false negative, but I do not care. I just want to be certain that I will never run a program that will not halt. I just decided: “will definitely halt for my purposes” even though the halting problem is unsolvable in general. This is generically true and is why formal methods work at all.

Veserv 3y ago

I do not see how that is relevant to my statement that formal methods, as required by the higher Common Criteria levels, do not constitute “box-ticking exercises”. Or are you arguing that these standards which require proofs of correctness are useless because proofs of correctness are much less impressive than box ticking?

astrange 3y ago
They are extremely expensive box ticking exercises. Furthermore, I don't think anything except box ticking exercises exists or could ever exist. You can only write down ways to make a process worse, not better.
- Veserv 3y ago
  I know that I have more confidence in a proven compiler that is thoroughly tested over a random compiler Joe the intern slammed out, but you do not seem to think that way. That is fine, you do you.
EVa5I7bHFq9mnYK 3y ago
Nothing realistically complex can be proven "correct". There is even a mathematical theorem about it - given a program's code, one can't even prove that it ever stops. One can, of course, apply proof of correctness to simple curcuits, where all possible inputs and outputs can be enumerated.
- Veserv 3y ago
  That is a complete misunderstanding of consequences of Rice’s theorem which generalizes the halting problem. You can not prove non-trivial properties about all programs that could could ever exist with no false positives or false negatives. You can prove non-trivial properties about almost every program. For instance, if I want to disallow programs that will not halt, I can just reject any program with a unbounded loop. I may also reject programs with a unbounded loop that will halt, a false negative, but I do not care. I just want to be certain that I will never run a program that will not halt. I just decided: “will definitely halt for my purposes” even though the halting problem is unsolvable in general. This is generically true and is why formal methods work at all.