I'm generally skeptical of gradual/optional typing. The reason is this: It's really, really hard to design a good type system after the fact. There are some pr

I'm generally skeptical of gradual/optional typing. The reason is this: It's really, really hard to design a good type system after the fact. There are some pretty compelling theoretical reasons for this (Rice's theorem) and also a fair amount of history of mediocre results. With OCaml/Haskell, not only do you get strong, static types, but the compiler can figure them out on its own. There's just no way that can happen for python. I've seen more compelling gradual/optional type systems. Last I checked, MyPy still had structural types as a "someday" thing. This puts a huge percentage of python code in the position of basically needing to be rewritten to be usable with MyPy. TypeScript has interfaces, and generally looks better put together to me. Racket takes an interesting approach, where whole modules are either typed or untyped, and it's pretty strict about enforcing things at the border: * If you import something from an untyped module into a typed module, you have to specify the type. * If you call a typed function from an untyped module, the type is checked dynamically. So you get much better guarantees. Erlang's dialyzer takes an interesting approach -- rather than being a conservative type system (where if a program type checks it is definitely type-correct), it is optimistic, so it will only bother you if it's sure it's found a problem. This lets you graft it on to existing programs without having to do major refactorings of parts that don't fit. But you lose a lot of the assurance that way. Still, my impression is it sees wider adoption (as a percentage of Erlang users) than any of the conservative gradual type systems I've seen. I haven't actually tried any of those beyond tens of minutes of playing around though.