[layer8]

Types are effectively assertions about the values they represent, and statically-typed code constitutes proofs that the assertions actually hold at runtime. The static typing forces you to be sufficiently rigorous in those proofs, which may require additional code as you mention. Without static typing, one has to rely on the "proofs" in one’s head to be correct (which humans aren’t really good at), instead of having the compiler double-check one’s reasoning.

[andybak]

I think this falls into the category of "The benefits of explicit typing are obvious and clear". It's the other side of the equation that I'm intrigued by and struggling most to formulate.