That's basically wrong. Type systems are driven by something that is much harder and much more valuable than optimization: writing correct programs. Optimizatio

That's basically wrong. Type systems are driven by something that is much harder and much more valuable than optimization: writing correct programs. Optimization is "strictly" less important than correctness, which means that there is no amount of improvement to optimization that is worth any loss of correctness. Okay, okay, there are a million caveats and side-notes to this, as there always are. This topic could (and does) fill textbooks. Let's get just a few out of the way: * Accepting lower precision in results is, of course, often done in the name of optimization. In these cases, there is a narrow band of "acceptable" outcomes; a small level of acceptable error that is still called "correct enough", so I'd argue correctness is still massively at a premium. In 3D games, very minor graphic artifacts on the level of 1% loss of "quality" are acceptable if it means a 5x speedup; 2% is probably not. So accuracy is "merely" 5,000 times more important. Getting within a factor of 10^-6 of the "true" result is acceptable in numerical analysis if it results in a 10x speedup, so accuracy is "merely" 10,000,000 times more important. * New graduates and entrants into software development massively over-prioritize optimization and performance, largely because the techniques to accomplish it are a lot more generic (and therefore teachable, and therefore over-represented in their classes) than the techniques to get correct behavior, which is highly specific to every domain. O(n^2) vs. O(log(n)) matters, but as long as you're hitting the correct complexity classes, performance is just not a big deal -- almost always, almost nobody cares. The (1 - almost)^2 times it does matter, you often drop down a safety level and work around the type system. * Static type systems have massively more power to help ensure correctness (by proving certain classes of errors aren't happening) than to improve optimization. You can mathematically prove that your type system prevents X, Y, and Z, and it's up to the programmer to decide if that's worth the restrictions your type system imposes. But optimization? That's all done through thousands of unrelated heuristics that may or may not help, increase the "quirkiness" of your compiled code, are a big source of compiler bugs, and depend on how the programmer writes the code. It is theoretically impossible (halting problem) to prove that any given heuristic is actually helping. Note that you can have a (valuable and loved) type-checker that is not actually a compiler (e.g. TypeScript's). As a rough, 90% correct soundbite: correctness is hard for people but easy for compilers; performance is easy for people but hard for compilers. This is why the few people who are working on bleeding-edge performance tasks are not using higher-level languages that are pushing the boundaries of type theory. They are using C and assembly.