On 7/12/07, Donn Cave <[EMAIL PROTECTED]> wrote: > In article <[EMAIL PROTECTED]>, > Ben Finney <[EMAIL PROTECTED]> wrote: > > > Paul Rubin <http://[EMAIL PROTECTED]> writes: > > > > > The idea of designing languages with more and more support for > > > ensuring program correctness is to put the established, repetitive > > > processes into the computer where it belongs, freeing the programmer > > > to be innovative while still providing high assurance of that the > > > program will be right the first time. > > > > This seems to make the dangerous assumption that the programmer has > > the correct program in mind, and needs only to transfer it correctly > > to the computer. > > > > I would warrant that anyone who understands exactly how a program > > should work before writing it, and makes no design mistakes before > > coming up with a program that works, is not designing a program of any > > interest. > > I don't get it. Either you think that the above mentioned support > for program correctness locks program development into a frozen > stasis at its original conception, in which case you don't seem to > have read or believed the whole paragraph and haven't been reading > much else in this thread. Certainly up to you, but you wouldn't be > in a very good position to be drawing weird inferences as above. > > Or you see original conception of the program as so inherently > suspect, that random errors introduced during implementation can > reasonably be seen as helpful, which would be an interesting but > unusual point of view. >
You can't prove a program to be correct, in the sense that it's proven to do what it's supposed to do and only what it's supposed to do. You can prove type-correctness, and the debate is really over the extent that a type-correct program is also behavior-correct. Personally, I remain unconvinced, but am open to evidence - I've only heard anecdotes which are readily discounted by other anecdotes. I absolutely do not believe that pure functional style programming, where we shun variables, is the best model for computing, either now or in the future. -- http://mail.python.org/mailman/listinfo/python-list
