Type enforcement can be static, catching potential errors at compile time, or dynamic, associating type information with values at run-time and consulting them as needed to detect imminent errors, or a combination of both.
In 1994, Andrew Wright and Matthias Felleisen formulated what has become the standard definition and proof technique for type safety in languages defined by operational semantics,[4] which is closest to the notion of type safety as understood by most programmers.
Many languages, on the other hand, are too big for human-generated type safety proofs, as they often require checking thousands of cases.
Nevertheless, some languages such as Standard ML, which has rigorously defined semantics, have been proved to meet one definition of type safety.
An early version of Sun's Java virtual machine was vulnerable to this sort of problem.
But most languages enforce the proper use of abstract data types defined by programmers even when this is not strictly necessary for memory safety or for the prevention of any kind of catastrophic failure.
Pierce says, "it is extremely difficult to achieve type safety in the presence of an explicit deallocation operation", due to the dangling pointer problem.
[13] However Rust is generally considered type-safe and uses a borrow checker to achieve memory safety, instead of garbage collection.
To resolve these conflicting goals, Ada confines type-unsafety to a certain set of special constructs whose names usually begin with the string Unchecked_.
SPARK avoids the issues with dangling pointers by disallowing allocation at run time entirely.
Ada2012 adds statically checked contracts to the language itself (in form of pre-, and post-conditions, as well as type invariants).
The C programming language is type-safe in limited contexts; for example, a compile-time error is generated when an attempt is made to convert a pointer to one type of structure to a pointer to another type of structure, unless an explicit cast is used.
(Something like printf("%s", 12), which tells the function to expect a pointer to a character-string and yet supplies an integer argument, may be accepted by compilers, but will produce undefined results.)
This is partially mitigated by some compilers (such as gcc) checking type correspondences between printf arguments and format strings.
It has support for untyped pointers, but this must be accessed using the "unsafe" keyword which can be prohibited at the compiler level.
In this case if the division has no finite representation, as when one computes e.g. 1/3=0.33333..., the divide() method can raise an exception if no rounding mode is defined for the operation.
Hence the library, rather than the language, guarantees that the object respects the contract implicit in the class definition.
However, some implementations, including Standard ML of New Jersey (SML/NJ), its syntactic variant Mythryl and MLton, provide libraries that offer unsafe operations.
These facilities are often used in conjunction with those implementations' foreign function interfaces to interact with non-ML code (such as C libraries) that may require data laid out in specific ways.
Another example is the SML/NJ interactive toplevel itself, which must use unsafe operations to execute ML code entered by the user.
[16] There still remained unsafe facilities such as the type cast syntax and variant records (inherited from Pascal) that could be used without prior import.
A Common Lisp compiler is responsible for inserting dynamic checks for operations whose type safety cannot be proven statically.
The problem could have been avoided by instead writing float fval = ival; The next example shows how object references can be incorrectly downcast: The two child classes have members of different types.