Thread by @unclebobmartin

Software is more like science than mathematics. Mathematical expressions are provable, scientific theories are merely demonstrable. Math is deductive. Science is empirical.

Software is empirical. We demonstrate, but do not prove, correctness.

Static typing is an attempt to make software more mathematical. Type correctness is deductive and provable. However, type correctness does not imply behavioral correctness. Even when fully type correct the behavior must be demonstrated empirically.

This doesn’t make type systems useless. On the contrary, many people find type systems to be invaluable. However, it does mean that type systems do not change software from a science to a mathematics. In the end, software remains an empirical science.

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.

Every feature is a theory. Every such theory is verified by a battery of experiments in the form of tests.

If you can write the code for the theory of a feature, you can write the tests are are the experiments that demonstrate that feature.

Science, FTW!