Project Focus and Goals

The project remains focused on logic-based tools to support programming and on implementing formal computational mathematics; we see these as inextricably linked activities. Over the years the scope of the project has expanded - from developing individual programs and theorems to constructing systems and theories. Starting with the slogan "proofs-as-programs," we now talk about "theories-as-systems." This change of scale has led to a new class of problems and challenges discussed throughout this project summary.

We are interested mainly in rigorously specifiable properties of programs and systems; for example, in showing that a communication system can detect when all processes in a group have received a message, or showing that the processes can elect a new group coordinator when the active one fails. We might want to show that a program solves an equation or builds a new basis for a vector space.

To know that a program actually satisfies a precise property requires knowing facts in a logical theory of programs and data. Many of the key facts are mathematical theorems about abstractions - like process groups - or about data structures such as graphs - or about a class of equations. These theorems are inextricably linked to theorems about numbers, lists, trees, sets, ordered pairs, graphs and all the other basic mathematical concepts.

To know about properties of programs, we must know about a large fragment of computational mathematics. Much of this knowledge is simply taken for granted by programmers and designers, but the formal tools need access to it as well.

We are currently focused on these goals:

Build proof assistants that are as indispensable to programmers and mathematicians as word processors are now.
Design and implement proof assistants that consistently exhibit problem solving behavior considered "intelligent" - in the sense that Deep Blue is an "intelligent" chess player. The state of affairs we are striving for is one in which:

proof assistants are full partners in solving major open mathematics problems such as P = NP?
proof assistants fill in or instantly recognize inference steps that are considered obvious by well-educated users, and they also routinely "discover" unexpected solutions to problems

Our strategy to achieve this "intelligent behavior" is to include the best problem solving heuristics; make them fast; and integrate them with the symbolic algorithms and data bases of mathematical knowledge.

Create consistent standard formalizations of the core mathematics that are widely assumed as background in computing and mathematics education at the college level and that are frequently used in designing algorithms and systems;

standard data structures and algorithms - numerical, symbolic, algebraic, geometric, logical, etc.
the mathematical semantics of programming languages, reactive systems, problems solving environments, etc.
mathematical models of physical systems and social systems (economies, populations).

Our strategy for this task is to use the most expressive formalism consistent with our goals. A key requirement is that the logical theory is able to express computational ideas and distinctions. Our priority has been to provide maximal expressiveness and then figure out how to automate it well.

Provide convenient access to the digital libraries of formalized mathematics; access that is so useful that the formal material becomes a standard reference for mathematical knowledge and is widely cited in textbooks. This will entail:

writing definitions, claims, theorems and proofs that are easy to read and understand
enabling major theorem provers to share libraries of mathematics so that a large amount of material can be accumulated and indexed
providing extensive cross-linking and indexing of the formal material, including connections to informal text.