Insightful +1. But by "types", they really mean the so-called practical languages' types, not the academic definition. Types allow you to prove something about

Insightful +1. But by "types", they really mean the so-called practical languages' types, not the academic definition. Types allow you to prove something about your program - but it takes extra upfront effort to prove something. The trade-off between ease and proof-power has settled on what we have... IDK of course, but I don't think it will change much. And worse, the popularity of static typing is mainly due to performance, followed by documentation, and correctness of proof not really in it. But maybe this story's empirical github evidence on errors will shift it a little. When you're re-coding all the time, the upfront cost isn't amortized over future runs as much as it used to be. Libraries are, but the massive real-world crowd-testing (i.e. usage) catches them... BTW I really like units of measure types, you get dimensional analysis almost for free. You can do it in e.g. java but it's verbose (i.e. it's java). Classes, with arithmetic methods (add, sub, mult etc), You need an ezplicit class for each unit combination (though you can do a little better with generics). And get compile-time type errors when you assign, compare or operate incorrectly.