> Python types are unprovable, since the type of a variable can change at runtime
You can certainly statically identify places where such changes are possible and the possible changes, in fact, Python static typecheckers do this.
> It's the Halting problem.
The Halting problem is a real thing, but you can simply bail out on any path that reaches a certain depth without resolution and fallback to the broadest possible type (failing narrower constraints) to avoid it.
You can identify some places changes are possible, but the problem is fundamentally unprovable, because of the Halting problem. You can't just hand-wave that away by saying, "we can use tricks to get 95% coverage." Ok, but if the type graph is not a provable entity that you can derive without simulating the program, you've sacrificed the fundamental point of C-style types, and that means you can never operate on them in the same way you can with C.
You can certainly statically identify places where such changes are possible and the possible changes, in fact, Python static typecheckers do this.
> It's the Halting problem.
The Halting problem is a real thing, but you can simply bail out on any path that reaches a certain depth without resolution and fallback to the broadest possible type (failing narrower constraints) to avoid it.