Hi Juan,

Thanks for probing further on this.

To give it a fair shake, I took a program in Racket that I've been working on for two years, it has an extensive test suite around it, so I know it is functionally correct. I decided I'll take one of the modules this evening and try to type check it (very easy to do in racket since you can switch from untyped to typed by changing a single line in your program). The net overhead of satisfying the type checker would then be my total cost of using a type checker, but its benefit would be zero.

It's basically a vector library with lots of higher order functions for machine learning. So this module isn't terribly big, about 256 lines total with about 150 lines of actual code, with an additional 100 lines of code with about 50 tests. It may have taken me maybe 3-4 hours to write the code and write tests for it in total. It's very easy in racket to convert from untyped to typed, so I did the conversion. The Racket type-checker is pretty much state of the art, so it's not a primitive tool by any means.

The type-checker threw 74 errors at me for no reason that I can see (most of the time it couldn't figure out the types so it wanted me to declare some stuff, in some other cases it needed some more restructuring and declarations). Assuming that it takes roughly 5 minutes to deal with each of these type errors, I'm looking at a total overhead of 370 minutes, which is roughly 6 hours. Let's be generous with my ability to debug type errors and half that amount. 3 hours. i.e., The time spent on delivering the module has doubled, and the benefit I have is exactly 0. So right now, my type-checker has a net negative overhead of 50%. Even at 1 hour (which in my experience is an outlier since chasing down type errors requires tracing the code quite deeply), it would be a significant overhead of 20%.

Yes, arguably this is one module in one program and hardly a scientific experiment, but it is quite typical of my experience with type-checkers. I spend as much time trying to satisfy the type checker as I do writing the code and tests. And that time is just wasted because any benefit I would have gotten from it I will get any way from writing tests. And I have to write tests in either case since types are hardly correctness guarantees.

I would very much encourage you to try experiments like this yourself. We can compare notes in the future. But you'll have to use a language like Racket to easily switch from typed to untyped and back ... Who knows, you may never switch back to typed :)