In moving from the untyped lambda calculus to the simply typed lambda calculus, one loses the ability to have non-halting programs. For me this just illustrates a fundamental point of type systems: limit the possibilities to make them understandable. Clearly I cannot describe a typical server with the simply typed lambda calculus, I need some kind of `while true: do()`.

With dynamic typing, it is easy to make programs that work with types that are extremely difficult to describe and comprehend. I think that is what TypeScript has added so much advanced type theory level functionality: it is necessary to describe what people did with dynamically typed javascript. I imagine MyPy and company will have a similar trajectory for python. People did some really incredible things in these dynamic languages, things which are very difficult to describe formally.

Meanwhile, it seems to me at least part of the point of some statically typed languages is to force people to work with simpler type systems to solve their problems. Because those simpler types may be easier to understand even if they require more effort or more code to solve the same problem. I do think Go was far too adamant for far too long about not needing generics (also known as parametric polymorphism); seems sober minds clearly disagree about where to put the boundaries. To me it seems that statically typed languages embrace the notion of "Good enough, but not perfect." They provide enough expression to solve problems, but not enough expression to describe all solutions.