Your contrived example is a bad smell in ANY language. No sensible coder ever writes a function that accepts both numbers and strings - handling multiple types should be done through proper polymorphic constructs, not arbitrary conditional branches.

There's a wide spectrum of correctness guaranties in programming - dynamic weak, dynamic strong, static, dependent, runtime validation & generative testing, refinement types, formal verification, etc.

Sure, if your domain needs extreme level of correctness (like in aerospace or medical devices) you do need formal methods and static typing just isn't enough.

Clojure is very fine, and maybe even more than just fine for certain domains - pragmatically it's been proven to be excellent e.g., in fintech and data analysis.

> Can't you see that unless you test every path ...

Sure, thinking in types is crucial, no matter what PL you use. And, technically speaking, yes, I agree, you do need to know all paths to be 100% certain about types. But that is true even with static typing - you still need to test logical correctness of all paths. Static typing isn't some panacea - magical cure for buggy software. There's not a single paradigm, technique, design pattern, or set of ideas that guarantee excellent results. Looking at any language from a single angle of where it stands in that spectrum of correctness guaranties is simple naivety. Clojure BY DESIGN is dynamically typed, in return it gives you several other tools to help writing software.

There's an entire class of applications that requires significantly more effort and mental overhead to build using other languages. Just watch some Hyperfiddle/Electric demos and feel free to contemplate what would it take to build similar things in some other PL, statically typed or whatnot. https://www.youtube.com/watch?v=nEt06LLQaBY