[ComNik]

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.

[pklausler]

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.

[ComNik]

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.