Nuprl is a formal methods tool. It embodies many of the basic ideas of this subject. The area is still a small part of CS in North America; a larger part in Europe. But it is increasingly seen as critical. The President's Commission on Critical Infrastructure Protection is an example of the growing awareness of the problems that formal methods were created to solve.
This area is not as well defined as AI or Automated Deduction or even Formalized Mathematics. Some people might question calling it a subject area because they prefer to think of it as an approach to software engineering and digital systems. It might be part of Software Engineering in that view. It includes the topics of Specification Languages; Formal Semantics; Formal Verification; Model Checking; and Programming Methodology. It will include the topics covered at meetings such as CAV (Computer Aided Verification).
Good web postings on Formal Methods are:
In the 1970s researchers felt compelled to alert the computing community to what they saw as a "crisis" in its ability to understand and control software systems. The crisis was that we could not trust the software being built; we could not say what it was supposed to do; we did not know how to make it do what it should, i.e., be more reliable.
This crisis is still with us, and is now much more visible. For example, the Year 2000 Problem (Y2K), also called the Millennium Bug, was studied by Congress. It was much feared and ending up costing billions of dollars to fix ($500B from the United States Government alone; estimates of $71B for US industry, estimates of upwards of $600 billion worldwide.
Books like Ivars Peterson's Fatal Defect document the death and property loss attributable to software errors. Peter Neumann maintains a Web site on computer risks and he has written a book Computer-Related Risks.
The response to the 1970s alarm has been the development of formal methods as an area of computer science. There is a sophisticated theory that informs a "technology of trust". The PRL project has contributed to the science base of formal methods as well as to the technology. Here are some of the technical topics associated with Formal Methods.
Specification languages are formal languages for defining computing tasks precisely. Typically one thinks of declarative languages like the predicate calculus or other logical languages. But imperative languages are studied as well - such as finite automata (as in statecharts) and IO automata. Very high level programming languages are considered such as SETL. (Citations.) Languages such as constructive type theory allow a mixture of declarative constructs and imperative ones.
Some of the specification languages that have been studied and used in applications are the Anna (Annotated Ada) language associated with the Ada programming language, the Zed language based on set theory, and its successor the B tool. VDM, or Vienna Development Method, is a language associated with Cliff Jones and his colleagues. VDM and Z are being standardized as a result of their successful use in industry.
There are specialized languages for hardware specification. VHDL (Hardware Description Language) is a standard worldwide language for the design and description of electronic systems. VeriLog is another international language of this kind.
Formal verification is the process of determining that a program operates according to its specification. There are various tools for helping perform these verifications automatically. Nuprl is one of those.
Much of our work falls naturally into the formal methods categories. The Nuprl type theory is a full-fledged specification language, perhaps the richest one available in logical terms; it subsumes higher order logic and Z set theory. But it is not supported by industry for this purpose as is the B tool or its predecessor the Zed Specification Language. One of the main advantages of the Nuprl specification language is that it is integrated into the Nuprl prover and the Common Math Library and is supported by two special editors.
As we improve the editors, add natural language output from specifications and proofs, and as the Common Math Library accumulates more standard models (such as results about IO automata), the Nuprl specification language will become more attractive to industry.