>Note: This doesn't mean that type systems can prove _all assertions_ about a program, but type systems do indeed work as provers.
Type systems can verify certain properties about code much like a test does, but that's far from being a mathematical proof of program correctness (especially since compilers have, you know, bugs).
>This isn't necessarily true unless you test for all inputs (which tends to be infeasible in most cases).
No, it's necessarily true. The vast majority of type errors I experience get picked up during TDD. A small minority reach production.
It's very easy these days to write tests that cover an enormous range of inputs and outputs (e.g. see quickcheck).
I'd estimate that maybe 5% of errors I experience in production are type related (in a dynamically typed language). That's offset against quicker development time (which also eans ease of fixing the other 95%).
>I believe there is almost no overhead imposed by a static type system
I think that's wishful thinking.
>In practice I've never had a bug with the type system (that I'm aware of)
Which type system have you never had a bug with? I've dealt with several buggy, crappy type systems?
>In practice I've never had a bug with the type system
I've seen plenty of bugs caused by picking the wrong type.
>I've seen hundreds of bugs from incorrect test assertions.
So have I. Different types of bugs though. The kind which static typing doesn't help eliminate.