Type-safe languages allow you to check the correctness of a program by proving a theorem about it: it will never suffer from implementation-defined, unspecified (by the language) behavior. Because of this property, programs written in a type-safe language have many more traces corresponding to the programmer's intention, by default, than programs written in unsafe languages. The tradeoff is that the programmer can have a harder time expressing his intentions.