Seven deadly sins of talking about “types” (2014)

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…

Good points. However, I disagree with this: > But please, stop pretending that type-level programming is a desirable thing. It's a kludge, and hopefully a temporary one. Personally, I want to write all my specifications in more-or-less the same language I use to write ordinary code. It's the tool's job to prove correctness or, if it must, tell me that it failed. I don't see explicit type-programming as (always) a kludge; oftentimes it's the primary vocabulary for expressing certain ideas…