Tony Morris

Scientific theories are demonstrated through experiments. We trust those theories only when experimental evidence is so vastly overloaded that our confidence has so many nines that we can tolerate the occasional glitch.

In software those experiments are tests. We demonstrate correctness by executing enough tests to raise our confidence to a level that has so many nines we feel safe deploying.

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.