Exactly, you can ship software in unityped languages. Still, how do you express even such a simple thing as a generic list type in simply typed lambda calculus?

Exactly, you can ship software in unityped languages. Still, how do you express even such a simple thing as a generic list type in simply typed lambda calculus? It's just that dependent types enable you to express any invariants statically, without actually running the code. > You can construct a NEL (NonEmptyList) in any language. That's trivial. That's true, with the caveat of: this invariant only exists in your head and hopefully docs. When it's encoded in a type, your compiler gets awareness of this invariant as well. Then it's able to do things that were impossible before, it can catch bugs that you would not (e.g. due the sheer amount of source code). Even though there are other approaches to software verification, types are the only one that got mainstream adoption so far.