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

[Kay Schluehr]

On Jul 20, 6:45 am, John Nagle <na... at animats.com> wrote:
> Juergen Erhard wrote:
> > On proving programs correct... from my CS study days I distinctly
> > remember thinking "sure, you can prove it correct, but you cannot do
> > actual useful stuff with it".  We might have come a long way since
> > then (late 80s :P), but I don't hold out much hope (especially since
> > the halting problem does exist, and forever will).
>
>  The halting problem only applies to systems with infinite memory.

Sure. But knowing that memory is limited doesn't buy you much because
you achieve an existential proof at best: you can show that the
program must run out of memory but you have to run the program to know
where this happens for arbitrary input values. Moreover you get always
different values for different memory limits. So in the general case
you can't improve over just letting the program run and notice what
happens.