Python from Wise Guy's Viewpoint

[Daniel C. Wang]

Joe Marshall <jrm at ccs.neu.edu> writes:


> I think the static typers will be agree (but probably not be happy
> with) this statement:  There exist programs that may dynamically admit
> a correct solution for which static analyzers are unable to prove that
> a correct solution exists.

Agreed. However, if you allow the programer to explicitly guide the static
analyzers with hints. I think that set of correct programs that are
provablely correct under with a static analyzer and explicit programer
hints, is very small.

Type inference and type checking are different things. Inference will always
be incomplete or undecidable in ways that are probably quite annoying. Type
checking maybe be incomplete, but no more incomplete than modern
mathematics.