Thanks for treating my comment charitably, and for adding your experience. Type systems often seem to bring out the extremist in otherwise reasonable developers.

It's quite obvious that there are downsides to types that most developers are missing - because most developers seem to feel that they get massive benefit from types, but empirical studies seem to show that if there really are benefits, they are not massive.

I see the downsides in a few ways - they open up another avenue for 'architecture astronauting', they are not in fact accurate representations of the real world in many situations - you're dealing with files, or messages coming in from the network which are not typed, and even when they are (e.g. databases), they can change under your code while you're running. That's not to mention the points I made above around usually being an entirely different, hobbled language that gets sprinkled through your source code. Types encourage people to build ridiculous code generation pipelines during build time, and builds getting larger and flakier are about the worst thing in the world for fast iteration. I find the Smalltalk approach of coding in a live image really interesting, and I worry that obsession with types are closing off that kind of future. There's also the fact that your language, and particularly your type system constrains what code you write - like a programming version of Sapir Whorf, and most type systems are bad at expressing very high levels of abstraction. Scala had to invent a documentation tool that hid the real types of things because the type signature of higher order functions like map and reduce were scaring people.

I was interested in your opinion of Spec, because I'm aware of it and find it interesting, but I don't do a lot of Clojure so I haven't really used it practically. I liked that it aimed to address more than just verification - schemas, object generation for property testing, these things are all closely related to the general concept.

I think your ideas about a middle ground type system seem very interesting.

I saw recently that there's a version of Nim 'DrNim' that incorporates the Z3 theorem prover which allows you to assert and prove much more interesting things than typical type systems. It sounds fascinating.