Re: type safety
I believe that type checks are related to safety in the sense that we
can check some categorized errors, and decrease the burden of the
interpreter. And it is also pretty sure that unless the language is too
restrictive we cannot guarantee only on the basis of type checks that the
program is "safe". Take the example of array bound checking. We cannot be
sure that the program does not exceed the array bounds only on the basis of
static type checking.
But this neverthless keeps the importance of type checking as it is. As
the interpreter has to do much less checks than, it would otherwise would
have done, without a type checker.
And the need of type checking increases many fold with the scenario of
mobile code(e.g. class files) where the bytecode might have been corrupted
over the network.
And the point that once type checked the program being proclaimed "safe"
is very misleading if not taken in proper context. The "safe"ty has to be
defined first. And the type system will ensure that the program will obey
the rules such that the program is "safe" as defined.