I think I've found a concise definition for type safety. I found it on the C2 wiki, which is a great source for programming related info. Anyway here it is:
Any declared variable will always reference an object of either that type or a subtype of that type.
A more general definition is that no operation will be applied to a variable of a wrong type. There are additionally two flavors of type safety: static and dynamic. If you say that a program is type safe, then you are commenting on static type safety. That is, the program will not have type errors when it runs. You can also say that a language or language implementation is type safe, which is a comment on dynamic type safety. Such a language or implementation will halt before attempting any invalid operation.
Taking the first sentence. This rules out any type of conversion so int->float is type unsafe, it rules out any type of dynamic cast too. So that basically rules out C, C++, Java and C# as type safe. Moving on to the main paragraph we see that aswell as static type safety there is also the concept of dynamic type safety. Using this as our bench mark, still rules out C and C++, but deems Java and C# to be dynamically type safe (if we choose to ignore the issues surrounding conversions of primitives of course). This laxer definition of type safety also includes languages like Smalltalk, Python and Ruby. So all modern OO languages are dynamically type safe.
If this is true, what is the dynamic versus static typing debate all about? Is type safety an oxymoron? Reading on further on the C2 wiki:
There are various degrees of type safety.
This is different from TypeChecking.
See also StronglyTypedWithoutLoopholes, which is another term for (at least) dynamic type safety.
So using the "degrees of type safety" argument, Java could be said to be more type safe then say Smalltalk. This kind of makes sense, since even though Java is not fully static type safe, it is partially so. So type safety is relative. So you can rate languages on their degree of type safety. Statically typed languages are more type safe then dynamically typed languages generally. If you click on the link CategoryLanguageTyping you will find out that what we usually refer to as static typing isn't actually called static typing at all, the proper name is Manifest Typing, Static Typing means something else and includes Type Inference. Given the common use of the term static typing, I have chosen up to now not to use the proper term which is in fact Manifest Typng.
So what does all this buy us? At best we are partially type safe if we choose to use a language like Java. Partially? Is that useful? Either I'm safe or I'm not right? For example, when releasing to production, I can't tell the QA Manager that I believe my program is partially safe. He wants to know whether my program is safe.
So how do I know that my program is Safe? Well simple, I test it!
I could go into strong versus weak typing and the consequences, but the links are there if you're interested. No program is Type Safe, and to claim so is a bit of an oxymoron. IMO typing is no substitute for well thought out tests, but type checks can help to detect and track down bugs (either at compile time or runtime). Where I believe manifest typing is useful is in improving the readability of code, improving the comprehension of large systems, and improving tooling support for code browsing and editing. Examples of this is the code completion and refactoring features in Eclipse. Smalltalk has these features too, but with manifest type annotations, tools have that much more information to work with.
The downside of manifest typing is that all type systems use 'structural types'. Structural types are based on the structure of your code. Depending on the code annotations available, manifest structural types can limit expressiveness. This is why languages like Scala have invented a more expressive set of type annotations, to overcome the type constraints imposed by languages like Java. Strongtalk's type annotations are even more expressive. This had to be the case because the Strongtalk type annotations had to be applied to the existing Smalltalk 'blue book' library, and this was originally written without any manifest type constraints whatsoever. The other downside of manifest types is that your code is more verbose.
So ideally what you want is :
* Manifest type annotations that can express intent and do not constrain you (or no type annotations at all or type inference)
* Strongly typed without loop holes at runtime
* Tests that tell you whether your code is safe.
Type safe doesn't exist, and partial type safety is a poor substitute for the above!