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

[John Nagle]

Paul Rubin wrote:
> "Diez B. Roggisch" <deets at nospam.web.de> writes:
> 
>>>Which implies that even in ADA, runtime type errors are in fact
>>>expected - else there would be no handler for such a case.
>>
>>Well, yes, runtime errors occur - in statically typed languages as
>>well. That's essentially the halting-problem.
> 
> 
> Well, no, it's quite possible for a language to reject every program
> that has any possibility of throwing a runtime type error.  The
> halting problem implies that no algorithm can tell EXACTLY which
> programs throw errors and which do not.  So the language cannot accept
> all programs that are free of runtime type errors and reject all
> programs that definitely have runtime type errors, with no uncertain
> cases.  But it's fine for a language to reject uncertain cases and
> accept only those which it can rigorously demonstrate have no type
> errors.

    That's correct.  Speaking as someone who once implemented an automatic
proof of correctness system (here's the manual:
http://www.animats.com/papers/verifier/verifiermanual.pdf), the halting
problem isn't an issue.  If you write a program for which halting is
undecidable, the program is basically broken.

    The way you prove loop termination in the real world is to define
some integer value (you can also use tuples like (1,2,1,3), like
paragraph numbers) that gets smaller each time you go through the
loop, but never goes negative.

    Most type issues can be resolved at compile time if you can
see the whole program.

				John Nagle