> A sufficiently powerful static type system entirely subsumes dynamic typing, and there is quite literally nothing you can accomplish with dynamic typing that

> A sufficiently powerful static type system entirely subsumes dynamic typing, and there is quite literally nothing you can accomplish with dynamic typing that you cannot accomplish with such a static type system. After writing software using both dynamically and statically typed languages, this is the conclusion I have arrived at, and it feels like a no-brainer to me. Do you thing some existing practical, high-usability programming language has a sufficiently powerful type system in the way you describe? For me the big thing is that static type systems tend to be simultaneously too powerless to express what I need, and too laborious in demanding manual specification of things that I don't actually need to specify for the program to work. In a dynamic language with a good schema system like malli or spec in Clojure, I can have easily customizable verification that is opt-in.