PEP 3107 and stronger typing (note: probably a newbie question)

[Chris Mellon]

On 7/12/07, Donn Cave <donn at u.washington.edu> wrote:
> In article <878x9llv5x.fsf at benfinney.id.au>,
>  Ben Finney <bignose+hates-spam at benfinney.id.au> wrote:
>
> > Paul Rubin <http://phr.cx@NOSPAM.invalid> 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.