When testing software, does people prove some part of the program to work as they want like mathematicians prove their methods to be correct?
3
- 2$\begingroup$ I love this question and would love it to stay on the site, but you need to make clear in what way it is about teaching CS. Can you edit it to make this clearer? (Just use the little "Edit" link under the question.) $\endgroup$Ben I.– Ben I. ♦2023-07-31 13:35:53 +00:00Commented Jul 31, 2023 at 13:35
- $\begingroup$ This would contradict the halting problem. In particular Rice theorem $\endgroup$Rushi– Rushi2023-07-31 18:09:47 +00:00Commented Jul 31, 2023 at 18:09
- $\begingroup$ @Rusi The halting problem doses not prove that you can not determine weather a program halts. It only proves that it is trivial to construct a program that can not be proven. $\endgroup$ctrl-alt-delor– ctrl-alt-delor2023-08-05 20:33:53 +00:00Commented Aug 5, 2023 at 20:33
Add a comment |
1 Answer
$\begingroup$
$\endgroup$
1 Yes, in theory, but not in practice.
The problem is that a "proof", like a program, might be flawed.
Some things, however, aren't amenable to proof if they depend on things that can't be controlled (race conditions, for example). Modern hardware is much more complex than simple models imply.
Don Knuth once said of an algorithm: "Beware of bugs in the above code; I have only proved it correct, not tried it."
In theory, theory is the same as practice, but not in practice.
- 1$\begingroup$ Depends on your view of the practice. In my view there are well-published examples of program verification, including verified compilers (eg CompCert and CakeML) and operating system kernels such as seL4. The proofs are machine checked. Contrary to your claim, concurrent programs, including those containing races are amenable to verification, too. $\endgroup$Kai– Kai2023-08-01 01:13:41 +00:00Commented Aug 1, 2023 at 1:13