One language that enforces strong typing is Ada. It has compiler-time and run-time type checking. It also had many other features to make the code less error-prone and maintainable. It was used by the DoD and also used in critical applications, such as nuclear power plants. The early versions of Java reminded me very much of Ada.
As far as I know, there's no runtime type checking of Ada, but there is runtime value checking to ensure values are within the specified ranges/adhere to the specified predicates (a very cool feature; you can specify that a type is always even, and encountering an odd value will cause an exception).
Oh, there is runtime type checking, though usually it is optimized out at compile time: it is for subtypes (which is mostly range checks) and checks of tags for tagged types (usually in class wide subprograms). Though both of them are often optimized out.
I'm hoping programming grows up enough to remember languages like Ada. Dynamic languages are useful for "get something running quick, then work on getting it right". Ada makes you get it right up front, or it doesn't even compile. The former is good if you have to bang out a script this afternoon; the later is good if you have to maintain a code base for 10+ years, with multiple programmers, and some assurances about reliability.
