Sure, but it's about striking a balance between the type (specification) and the program (implementation). The myth mentioned is just something people say to beginners in Haskell but no experienced programmer truly believes - reason being again this balance.
When you can express so much in your type system that the implementation can be mostly automated, you have shifted the semantic mess to a level above but have not really made any substantial progress. Still, it's undeniable that type systems are perhaps the only kind of formal methods who really made it to the mainstream software developer because they can be useful. What I find frustrating is that no one is really guiding the programmers in finding good patterns for achieving a healthy balance specially for code that needs to be maintained and adjusted to new use cases.
I'm not sure they have become mainstream. Java and the like have Generics, but I think that's about where "mainstream" ends. (And even Generics can be problematic).
I think many programmers are skeptical of advanced type systems because the OPs straw man is what gets advertised at the water cooler. I've seen it myself in professional settings.
My impression is that advanced type systems interest people because they're cool moreso than because they're practical tools for reducing errors.
The kind of discussion I see on this post generally reinforces my impression.
