I'm guessing you've never actually proven type safety for a non-trivial language, if any. While there are many ways type safety could be stated for Scala, I'm pretty sure most Scala programmers would like the version of type safety that states "if I never use a type cast, I can never get a class cast exception." If you think that is too strong of a statement, then fine, but I think most people would agree this is a reasonable expectation for Scala.