On 29/07/2010 19:49, Walter Bright wrote:
Don wrote:
I agree with Walter's statement that ALL of the components are
unreliable, and I think it's important to realize that proofs are the
same. Even in the case where the program perfectly implements the
algorithm, there can be bugs in the proof.
Also, the hardware running the correct program can fail.
Yes, but that's a different issue. It would still be of value to know
that the program is correct. For example, you could make a reliable
system by having several different hardware run the same program and
compare the results. This is similar to what you said before about
achieving redundancy, but here you would not need other separate teams
to write a different programs to compute the same thing, which obviously
would be a great saving in effort.
I'm not going to argue if it is possible, or practical, or whatever to
know for sure that your program is correct. My point is just that
knowing with absolute certainty that a program is correct, that would
still be quite valuable, regardless of the fact that hardware, or other
programs, systems, etc., could fail.
--
Bruno Medeiros - Software Engineer
