I agree that the third point is important, but it's not clear that it's static typing that is important, and not type annotations. One reason why I can still fairly easily read and understand Eiffel code that I wrote decades ago is Design by Contract. And there's normally nothing static about DbC, it's about assertions that are checked at runtime and that by convention are part of a class's interface.

What both type annotations and DbC are is self-enforcing documentation (of an interface) that doesn't go out of sync with the actual code. But for that, you don't necessarily need static type checks. Now, type checking of type annotations that happens exclusively at runtime is an option that hasn't been explored much (after all, if you already have type annotations, why not let the compiler make use of them?), but an option that has sometimes been used successfully is having a mixture of static and dynamic type checks. You can often greatly simplify a type system by delaying (some) type checking until runtime (examples: for covariance or to have simpler generics).