Programming without a proper strong type system is like trying to build a house without knowing where any of the other bricks are. It is like placing bricks in space guided only by memory. Is there a brick underneath? You cannot see. And only when you step back do you find if it all collapses – then you have to search for which brick was unsupported.
One can oppose type-checking with visibility, and suggest visibility is preferable. Instead of static typing, build iteratively with small chunks, as is the culture of Lisp or Smalltalk. Why do you need to have things checked when you can see what you are doing?
Typing (static) is about ensuring coherent action. It is about maintaining consistency of intention: meaning the same thing with the same names in different parts of the software.
Visibility seems to be doing the same thing – it is a way of ensuring consistency too.
But the visibility here is execution: you run the software, quickly and often, in small chunks, to see what it does. This kind of visibility is inadequate because it is too specific. In software, we want control of abstractions, but execution is only showing particular cases.
By designing software, we are making assertions about abstractions – that is, whole sets of practically innumerable cases. It is wholly the wrong approach to seek to prove or ensure this through individual cases. It is the very strength of software – in its material of abstraction – that we can reason about and control whole sets of things – abstractions.
Typing is about the abstractions themselves. It addresses the fabric of construction where the visibility of execution does not.
Typing is a kind of visibility and a kind of execution. But it is for the right kind of thing – the logical structure of abstractions. It executes something to test the structure of the abstractions. It is a kind of internal, or higher-level execution.
Typing does something distinct from iterative trialling or testing, and something important.
Programmers should have immediate indication of what and where things are. And they should be looking at the abstractions, not the instances: we want to see not a few points, but the curve of the graph.
Strong typing is itself not enough. We should be shown we are right or wrong immediately as we form the code (even the Sinclair ZX80, and descendants, was right.).
But neither is that quite right. Really we should only be able to make valid and consistent transforms to the code.