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.
