[ryandv]

In a Turing complete dynamic language I believe that some properties of the runtime would be undecidable. The advantage of static typing is that many (most?) type systems are sufficiently constrained (i.e. not Turing complete) such that the typecheck procedure can be assured to terminate.

Of course, with sufficiently expressive type systems you end up with Haskell "UndecidableInstances" or Coq dependent types or C++ compile-time tetris, [0] and now you are back to the same problem as with analyzing the runtime. Otherwise you may find it difficult to encode the desired properties or invariants into your type system, for lack of expressive power... tradeoffs abound, and so on.

[0] https://news.ycombinator.com/item?id=9813800

[mdaniel]

Or my favorite alternative to that story: well, it's currently a str ... maybe it'll still be a str in 5 minutes, who knows

[ryandv]

In a dynamic language where code that produces such a side effect is admitted by the (lack of) compiler/typechecker, sure; however a static checker would probably ensure, before runtime, that said binding indeed refers to a str, now and forever.

But I realize now the point of ancestor's comment is that you don't have such a guarantee in a dynamic language - hence the tendency to lean more on REPL-oriented development, highly interactive live runtime environments, tight TDD feedback loops, etc...