3 ms·

"It is not sufficient merely to prove a program correct; you have to test it too." Well in fact it is exactly the contrary.

by lkuty 4y ago

User23 4y ago
It’s a clumsy formulation, but if what he means is that you need to be assured that the model you’re proving in accurately reflects the behavior of what is being modeled then he is correct at least sometimes. For example a naive Z3 proof of the mid procedure would be valid since Z3 ints are unbounded. The issue isn’t that the proof is wrong, it’s that the model is. If the system has a well written formal specification then your model can be built from that without error if done diligently. One real world example is the first Algol 60 compiler, which was built to a formal specification. On the other hand if there is no useful spec or no spec at all then you end up needing to experiment, ie test, and get your model as close as you can.
Jtsummers 4y ago
I took it as a reference to Knuth: "Beware of bugs in the above code; I have only proved it correct, not tried it." https://staff.fnwi.uva.nl/p.vanemdeboas/knuthnote.pdf https://staff.fnwi.uva.nl/p.vanemdeboas/knuthnote.pdf [PDF] page 7 of the PDF, 5 of the classroom note.
a1369209993 4y ago
No, what you've observed is the (IIRC the terminology) converse, namely: It is not sufficient merely to test a program; you have to prove it correct too. In addition, it is not sufficient merely to prove a program correct; you have to test it too. In summary, you have to both prove a program correct, and test it; skipping either will result in buggy garbage.
- joshuamorton 4y ago
  Grandparent is correct. If you've proven the behavior correct, you don't need to test. The proof is the test. This is usually only true in languages-that-are-proof-assistants (idris). In the cases above, they hadn't actually formally proven the behavior correct.

3 ms·

"It is not sufficient merely to prove a program correct; you have to test it too." Well in fact it is exactly the contrary.

by lkuty 4y ago

"It is not sufficient merely to prove a program correct; you have to test it too." Well in fact it is exactly the contrary.

User23 4y ago
It’s a clumsy formulation, but if what he means is that you need to be assured that the model you’re proving in accurately reflects the behavior of what is being modeled then he is correct at least sometimes. For example a naive Z3 proof of the mid procedure would be valid since Z3 ints are unbounded. The issue isn’t that the proof is wrong, it’s that the model is. If the system has a well written formal specification then your model can be built from that without error if done diligently. One real world example is the first Algol 60 compiler, which was built to a formal specification. On the other hand if there is no useful spec or no spec at all then you end up needing to experiment, ie test, and get your model as close as you can.
Jtsummers 4y ago
I took it as a reference to Knuth: "Beware of bugs in the above code; I have only proved it correct, not tried it." https://staff.fnwi.uva.nl/p.vanemdeboas/knuthnote.pdf https://staff.fnwi.uva.nl/p.vanemdeboas/knuthnote.pdf [PDF] page 7 of the PDF, 5 of the classroom note.
a1369209993 4y ago
No, what you've observed is the (IIRC the terminology) converse, namely: It is not sufficient merely to test a program; you have to prove it correct too. In addition, it is not sufficient merely to prove a program correct; you have to test it too. In summary, you have to both prove a program correct, and test it; skipping either will result in buggy garbage.
- joshuamorton 4y ago
  Grandparent is correct. If you've proven the behavior correct, you don't need to test. The proof is the test. This is usually only true in languages-that-are-proof-assistants (idris). In the cases above, they hadn't actually formally proven the behavior correct.