Since leaving academia and returning to "professional" software engineering, my opinion on productivity and type checking has reversed. I now believe that statically-typed languages (Java, C++, Go, Scala) are more productive for large software projects than dynamically-typed languages (Python, JavaScript, Ruby). If the program is small enough that I can fit it in my head, dynamically languages are better. However, once the program is big enough that I don't remember what I wrote last month, and other people are also making changes, compilers catch a lot of dumb errors (apologies to my co-founder Vijay Pandurangan, who stated it this way about a year ago, before I believed it). Part of it may be that most of my professional work has used static languages (mostly C++ at Google, C++ and some Java at MIT, now Java at Mitro). However, I've written lots of Python in my life, and at Mitro our browser extension is written in JavaScript. In both cases, I occasionally end up with bugs in production because I'm accidentally passing in the wrong arguments to a function, or I'm using the wrong variable or function name. These bugs are particularly amusing after a task has been running for 30 minutes, or when it happens on a customer's machine.
It could be that I'm "doing it wrong" (please tell me how to do it right, if that is the case!). Many companies write big programs in these languages, so clearly it is possible (Dropbox/Python, Facebook/PHP, Github/Ruby, etc). However, many of these uses are places where errors are can be fixed quickly, like web sites, which makes it cost less to fix runtime errors. For example, Etsy argues that fast deployments are critical to their software engineering productivity. However, even in these cases, I think the additional cost of making the compiler happy pays off by catching some errors when I write them, rather than when I'm trying to deploy my "finished" change.
To support my claim in a manner appropriate for a blog post, I will now include a random collection of other people who think the same way I do. Evan Farrer ported mature, unit tested Python programs to Haskell and found bugs, concluding that unit tests are not sufficient. John Carmack (Doom, Quake) claims that "The most important thing I have done as a programmer in recent years is to aggressively pursue static code analysis" (see also a tweet about types in Lisp). Bruce Dawson at Valve Software (Steam, Counter-Strike) has a similar story. Tim Sweeney (Unreal engine) argued that better type checking could improve productivity in his talk "The Next Mainstream Programming Language" (2006 at POPL). William Edwards recently claimed that "dynamic languages are unmaintainable", for similar reasons as me.