Full, formal verification of complex systems (especially in the distributed case) requires a lot of modelling effort, beyond what is needed for "mere" implementation. A lot of important constraints cannot even be expressed in most type systems. And if one uses a specialised modelling language for the proof, the actual implementation might introduce bugs.
Also relevant to real, shipping software: specifying a program in such that detail as required for automatic verification makes it even harder to change (which, given infinite time and money, is indeed a very very good property!).
This just goes to say, that a type system can be very helpful, but is ultimately just a part of regular testing.
So for most companies and most developers, anything that aides in keeping documentation up-to-date, writing or generating tests and helping developers understand what they are reading is probably a better ROI.
If static type systems cannot do everything, it does not make sense to me to conclude that they shouldn't then be used for anything. Type systems aren't part of "regular testing", they're part of compile-time error checking.
That was not the intension behind my comment at all. I rely on type systems a lot, myself.
I was trying to note that Clojure, as a dynamic language, is making a (to my eyes) very interesting choice, of doubling down on these dynamic methods of verification. For some uses, I can see this as the better choice, for others it isn't and won't be.
As I commented elsewhere, Clojure very deliberately adopts the stance that type systems like Haskell's are valuable but heavyweight, and chose development speed and concision over types.
In my own work, I chose Clojure because it mirrored my experiences: that type systems weren't worth the trade-offs for me and my field.
Would I prefer stronger typing in different domains (longer project times available, greater consequences of failure like medical devices, etc.)? Sure, and I have in the past. But it's not the case that dynamic languages are always the incorrect choice, like smoking cigarettes.
When you prove that a language like Clojure (untyped, but with dispatch that is no more dynamic than that of many modern typed languages) combined with a construct like specs is significantly less safe than any typed language, then you can make that statement. It's not like untyped and typed are two binary categories; otherwise, I could say that wanting less dangerous typed languages as opposed to formal tools are just like wanting less dangerous cigarettes. These ideas exist on a spectrum.
This just goes to say, that a type system can be very helpful, but is ultimately just a part of regular testing.
So for most companies and most developers, anything that aides in keeping documentation up-to-date, writing or generating tests and helping developers understand what they are reading is probably a better ROI.