Comment by phplovesong
4 months ago
Thats a bad analogy. A better one is should we check the breaks before (compile time) we start the car and drive down the highway (runtime).
At this point you either did check the breaks, or did not. If not you are out of luck if the breaks did infact not work.
Or you test the breaks as you stop to see that everything is clear as you exit your driveway and go into the street.
This sounds like the typical "its good enough" argument. Say we test the breaks manually nine times of of ten. This means we get really hard to diagnose bugs because "this did work when i tested locally". And users get more runtime errors because of half-assed development.
Type systems should be treated like maths, its either correct, or not. In the end, a typesystem is basically just that, its math behind the scenes, more specifically a genre of maths called category theory.