Firstly, they'd be written in the same language that you are coding in, not a weird, half baked type language, that adds visual noise to your code.
Secondly, they'd have much more power to define meaningful and useful behaviour rather than being restricted to talk about correct behaviour via types.
Thirdly, they'd run when you wanted the tests to run, and you could tier different tests to run at different times, so they aren't all slowing you down while you're doing fast iteration.
I used to like types, but then I realised that what matters is how quickly you see the bug. Seeing it in your code editor is brilliant, but if it's slower in time than hitting control S and seeing the actual app in the other pane auto reload, and fail or not, then it's worse.
These days I look on the idea that you know the exact types of all data your program will interact with at the time you write your code as the same sort of mistake that we made when we thought we understood the deep inheritance hierarchies of the real world.
I write a lot of Purescript and a lot of Clojure. Purescript, being basically a Haskell variant, is about closing down every last little part of the system into types. You _do_ pick up a lot of visual noise for this (like `liftEffect` ugh...). Whereas Clojure, is the polar opposite. It's about keeping the system open, using large chunks of data, and having functions take/change what they need and pass along everything else none-the-wiser to what's present.
Bouncing back and forth between these two worlds, I think I've begun to lean towards the opinion that I really only care about strict types at the boundaries of my program and certain very specific checkpoints along the way (generally, something like a module/namespace boundary).
Clojure has Spec, but it misses the mark in my opinion because it doesn't solve refactoring. It's not (currently) instrumented enough to help the me as a human make changes to the code without also just "bumping into the guard rails" to try and figure out what I broke along the way.
A middle ground orthogonal type system sounds really appealing to me. "Type coverage" is an idea I've been kicking around. Something like Spec in Clojure, but more symbiotic with the host code such that it can tell you things _about_ your code and help in refactoring, symbol resolution, etc..
That's a lot of words, but tl;dr I think I agree with you : )
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.
