[srean]

I think this something that needs to be experienced firsthand a few times for this to sink in. It something like the backpropagation update of a neural network: no matter how long you stare at it, it wont be clear, but if you derive it yourself it becomes super clear.

I can say that this effect seems very real. I think the reason goes beyond those shallow type mismatch errors I often make. Part of the reason, I think is, the correct program becomes clearer to write compared to the erroneous programs you could have written if you use the type system. In other words types can make some of the erroneous versions cumbersome, or at time, impossible to write -- but good luck mud wrestling with the compiler till its convinced.

I will strongly encourage that you try it and dont be discouraged. This really needs to be experienced first hand to be convinced.