I think the argumentation here is a bit a skewed towards 'what static types can and cannot do for the compiler' - i.e. how they can help the computer in constru

I think the argumentation here is a bit a skewed towards 'what static types can and cannot do for the compiler' - i.e. how they can help the computer in constructing formal proofs. For me another almost as valuable thing is how static types help me think about and design the code. The static type information is always there to remind "this entity belongs to this set of objects" which frees me from the cognitive burden of maintaining this constantly in my working memory. With specific static types the function signatures now document the tranforms defined for those entities . This aspect of static types as a cognitive tool is highly personal, and not same for everyone, unlike the language and the compiler, though.