&gt; Static typing ensures that some sliver of that knowledge is explicit and checked.<p>No.  <i>Testing</i> ensures that the knowledge is checked.  As in: run experiments.  Empirical evidence. Static typing only checks one set of assumptions against another set of assumptions. Don&#x27;t get me wrong, this is better than nothing. But the only real check is actually running the code, getting empirical evidence.<p>In every other engineering discipline, math is seen as a tool, simulations are <i>cost saving measure</i> because running experiments for everything is too expensive. Only in the discipline where gathering empirical evidence is actually generally <i>cheaper</i> than trying to prove things (with mostly dubious value) is there this odd notion that using math is superior to running the experiment.<p>If flying planes or running wind tunnel tests were as quick and cheap as running computer simulations, there would be no more computer simulations in aviation.<p>Compare Knuth:  &quot;Beware of bugs in the above code; I have only proved it correct, not tried it.&quot;