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.

That hasn't been my experience so far, but I'd be interested to read in more concrete terms exactly what level of type-level invariant expression begins to create overly-rigid software.

FWIW, I'm not suggesting moving everything possible into types. I'm suggesting types are better than not having them, just like tests are better than not having them.

A software artifact that has a very specific type usually also needs to be very specific in terms of its required preconditions. Which puts a significant burden on the user of that artifact. And now that user probably requires its own additional preconditions to be able to conform. And so on.

I don't know, maybe there is a good way of structuring the software to avoid this effect (I'm not extremely invested in type systems), but maybe it's just a lot of additional pain on top -- too much perceived pain for people who can barely make their software "seems to work".

I can confirm this 100%. Having worked at an old (19 years) Java code-base full of unnecessary patterns & abstractions. Even with really great refactoring help from the IDEA, making meaningful changes is very very time consuming. I've spent weeks on it. The complexity was creeping in over the years and is almost impossible to get out again. But it has types!!!11!

And if I then look at the actual data transformations behind all this code: It would be a 2 day exercise in Clojure to re-build this from scratch.

Java has probably the most notoriously limited typesystem in actual use. Judging type systems by Java is like judging electric cars by the Sinclair C5. Try an ML-family language sometime.

It will have the same intrinsic problems. It doesn't matter that it is Java.

Nonsense. How can you claim that without having seen or tried it?