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.
-
Show this thread
-
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.
10 replies 19 retweets 109 likesShow this thread -
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.
3 replies 10 retweets 50 likesShow this thread -
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.
2 replies 8 retweets 39 likesShow this thread -
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.
3 replies 9 retweets 71 likesShow this thread -
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.
11 replies 16 retweets 72 likesShow this thread -
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.
25 replies 8 retweets 59 likesShow this thread
Once again, you've made blatantly incorrect statements, undermining entire fields of mathematics and progress in research. Again, my invitation to help you learn why it is wrong, remains on the table. How do you feel about loud claims that deny the earth is an oblate spheroid?
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.