No matter in the academic circle or in the industrial circle, there are always many people who care too much about the so-called "correctness of the program", and some even go to the point of trembling and chasing after the end.
I agree with many of your points, but I also think what should be criticized are the people, not the methods, and you are also overgeneralizing about people. I am talking from the perspective of a researcher in formal methods.
The point of formal methods is definitely not to ensure 100% correctness.
- Theoretically, lightweight formal methods such as type systems and bounded model checking are sound but not complete; furthermore, the most general form of the verification problem is fundamentally undecidable.
- Practically, even if a theorem prover declares a program correct, this can be a false positive. Any stage can go wrong: there can be human mistakes in the model, the formal specification, the prover itself, and even the compiler.
You said that "people who talk about 'correctness' and 'reliability' every day are almost always high-minded, and they talk more than they do". Researchers in the field of formal methods certainly talk about correctness every day, but the unattainability of 100% correctness is a really common sense in the field.
Then what's the point of formal methods? -- to make it easier to write correct code, and to increase trust of a program that is also written. There are many critical systems that require extra evidence for correctness: chips, medical systems, aircrafts, etc. If the verifier says the program is correct, it is probably correct; if the verifier says the program is wrong, something must be wrong.
Regarding your "Riemann Hypothesis" analogy: if the Riemann Hypothesis is proved *wrong* by you, it is very likely that a theorem will be named after you. (By the way, I don't agree that "first-rate mathematicians propose conjectures, and second-rate mathematicians prove other people's conjectures". It's debatable whether or not Goldbach is a first-rate mathematicians, but many who have attempted his conjecture are undoubtedly outstanding mathematicians.)
To summarize, I agree that
- to talk about program correctness, one needs to write the program first;
- formal methods have many limitations, and the outputs may be false positives;
- testing (e.g. unit tests) can get extremely tedious, and some formal methods are not easy to use.
I don't agree that
- formal verification can only be done with toy-size programs (chip verification is an example; the verified C compiler is another example);
- advocating "testing" and "formal proof" every day cannot improve the correctness of the program (they can, when applied properly; unnecessary to advocate every day though); and
- people who emphasize program correctness are all talk.
1、Whether a program is good or not, the most important criterion is whether it can effectively solve the problem, not whether it is correct.
2、The emphasis on program correctness should never be higher than writing the program itself.
3、So I like to say that first-rate mathematicians propose conjectures, and second-rate mathematicians prove other people's conjectures.
4、In my opinion, the most effective way is to think and scrutinize the code to make it simple and intuitive, until you can see at a glance that there is no problem with it.
But it's also fine for some people to focus on solving the (right) problems, and others to help increase its correctness by researching and writing programs that analyse and attempt to prove or test.
Hi Yin,
I agree with many of your points, but I also think what should be criticized are the people, not the methods, and you are also overgeneralizing about people. I am talking from the perspective of a researcher in formal methods.
The point of formal methods is definitely not to ensure 100% correctness.
- Theoretically, lightweight formal methods such as type systems and bounded model checking are sound but not complete; furthermore, the most general form of the verification problem is fundamentally undecidable.
- Practically, even if a theorem prover declares a program correct, this can be a false positive. Any stage can go wrong: there can be human mistakes in the model, the formal specification, the prover itself, and even the compiler.
You said that "people who talk about 'correctness' and 'reliability' every day are almost always high-minded, and they talk more than they do". Researchers in the field of formal methods certainly talk about correctness every day, but the unattainability of 100% correctness is a really common sense in the field.
Then what's the point of formal methods? -- to make it easier to write correct code, and to increase trust of a program that is also written. There are many critical systems that require extra evidence for correctness: chips, medical systems, aircrafts, etc. If the verifier says the program is correct, it is probably correct; if the verifier says the program is wrong, something must be wrong.
Regarding your "Riemann Hypothesis" analogy: if the Riemann Hypothesis is proved *wrong* by you, it is very likely that a theorem will be named after you. (By the way, I don't agree that "first-rate mathematicians propose conjectures, and second-rate mathematicians prove other people's conjectures". It's debatable whether or not Goldbach is a first-rate mathematicians, but many who have attempted his conjecture are undoubtedly outstanding mathematicians.)
To summarize, I agree that
- to talk about program correctness, one needs to write the program first;
- formal methods have many limitations, and the outputs may be false positives;
- testing (e.g. unit tests) can get extremely tedious, and some formal methods are not easy to use.
I don't agree that
- formal verification can only be done with toy-size programs (chip verification is an example; the verified C compiler is another example);
- advocating "testing" and "formal proof" every day cannot improve the correctness of the program (they can, when applied properly; unnecessary to advocate every day though); and
- people who emphasize program correctness are all talk.
Looking forward to hearing from you.
Best,
R. C.
1、Whether a program is good or not, the most important criterion is whether it can effectively solve the problem, not whether it is correct.
2、The emphasis on program correctness should never be higher than writing the program itself.
3、So I like to say that first-rate mathematicians propose conjectures, and second-rate mathematicians prove other people's conjectures.
4、In my opinion, the most effective way is to think and scrutinize the code to make it simple and intuitive, until you can see at a glance that there is no problem with it.
But it's also fine for some people to focus on solving the (right) problems, and others to help increase its correctness by researching and writing programs that analyse and attempt to prove or test.