Of course, you can easily do things in a dynamic language that are observably correct, but which are very difficult to prove correct without advanced logic (i.e., an expressive type system). And more advanced type systems typically lose some nice ergonomic properties of simpler type systems, such as clear error messages, type inference, principal types, or decidability. So I can definitely see how someone moving for example from Java to Python would find the latter very liberating at first.
On the other hand, you can argue that people shouldn’t be writing code that’s so difficult to prove things about in the first place. :)
To my mind, the benefit of static types is that they allow proving properties of your code, but the cost is that they may force you to do so; the benefit of dynamic types is that they don’t force you, but the cost is that they don’t allow it.
On balance I think static types are therefore preferable, because you can always fall back to dynamic types (strings/hashes/variants/sums) in a static language, but you can’t “fall forward” to static types in a dynamic language.