Tony Morris

There is no escape from this. Whether you use static, or dynamic typing, you must still demonstrate correctness by executing tests. Static typing does not reduce that number of tests, because those tests are behavioral and empirical.

Thus, the testing burden is independent of typing. The number of tests you write and execute is unaffected by the type system of your language.

I can’t dispute that programs CAN be proved correct. I think the original assertion is that more often they are not, they are tested empirically using test cases. Anyone who works in the software industry and disputes that is just lying to themselves.

“testing burden is independent of typing” implies that types don’t prove anything worth knowing(or testing) about programs. If this seems false to one’s intuition, I’d recommend giving a modern type system the ol’ college try.

For the record: I’m pro types. I agree that types do mean that some test cases are not needed. However, rarely does it mean that no tests are needed to verify the behavior.

For sure, I think few would contest that. That’s very different from the original claim.