Static type-checking in Camelot guarantees RAM usage -- not only its safety but also its amount.This implies to me that type systems will become indispensible tools very soon. Once languages exist that use their type systems to prove properties like the above, today's programming languages will be as obsolete as wood burning steam engines.
Static type-checking in my controlled pi-calculus (definitely not a real programming language) guarantees statically properties of access control ("only X can use the printer", "I can only read this information for the purpose of transferring it to you", ...) or resource management ("this program will never require more than x threads, y RAM and z printers").
Static type-checking in TyPiCal guarantees the respect of some protocols. In Acute, you can check the safety of communications...