Software is becoming increasingly a vital element in diverse parts of people's life, from day-to-day communications to electronic commerce to home entertainment to medical surgery. New software is produced and existing software updated, all at a rapid pace unimaginable 10 years ago. The environment makes it imperative for designers and corporations to deliver software with proper and safe behaviour. As an example, consider a software company which distributes an e-commerce package to a large number of users connected to a broad-band network (the software itself will be distributed via the network). Many personal transactions will be performed using the package, so that if it causes a security hazard such as leak of private information, the maker/distributer of the software may well face threats of litigation. Because of the complexity of modern software (which may involve not only numerical calculation but also access to resources such as files, use of OS routines and communication with resources and software distributed over the network), it is getting increasingly hard to rely on informal engineering principles alone for ensuring crucial properties: we need a general and rigorous framework for controlling and ensuring safety of programs based on fundamental mathematical principles.
The need of a mathematical basis for software safety has been observed by many significant researchers in the programming language community in the past few years. For example, an article on language-based security [34], written by the authorities in the field, makes a convincing case for its needs. Already many researchers in industry, for example those working on security of Common Language Runtime, one of the Microsoft's most basic components of its whole range of operating systems, are actively engaged in the development of such formally founded safety technologies.