I don't think it's accurate to compare type systems and mathematics. When you write out a mathematical equation, you don't explicitly specify if the variable is

I don't think it's accurate to compare type systems and mathematics. When you write out a mathematical equation, you don't explicitly specify if the variable is a float or an integer or a set or a vector or a matrix as part of the equation, the reader will infer the type of each variable from the problem domain. So in fact, math is much more like dynamically typed languages. >> We know types help us eliminate certain classes of errors from programs. Yes and in my experience they often also introduce new kinds of errors, architectural errors (which are much worse). If you have a system which makes it easier for developers to pass around complex instances across multiple source files, they will use that feature and it will often lead to modules which have lower cohesion and tighter coupling which adds complexity and makes it harder to modify and maintain the logic in the long run. Rigid type systems also add complexity when integrating with third party modules which may use different type names for similar concepts. The wisdom of dynamically typed languages is precisely that it is difficult to know what the type of each variable is so it forces you to follow the logic around (which is unpleasant but necessary). What is almost always overlooked is the human psychological effect; this unpleasantness involved in trying to keep a mental picture of the logic creates a strong incentive for developers to keep the logic as simple, modular/encapsulated as possible. This results in better software design/architecture overall. I'm saying this based on decades of experience having gone back and forth between dynamically and statically typed languages. Programming is as much about human psychology as it is about logic. Dynamically typed languages force developers to be more disciplined and this mindset is extremely valuable. Statically typed languages tend to put developers on auto-pilot. You get so caught up on types and catering to the compiler's warnings that you lose some common sense. Coding in a statically typed language feels a bit like having a boss who micromanages you and tells you every little detail that you need to implement. Coding in a dynamically typed language is more like having a boss which tells you the general picture of what is required and lets you figure out the details. I think the mindset of self-reliance which comes with dynamically typed languages is very important when it comes to producing high quality code.