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

[Paul Rubin]

"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.