The Nature of the PRL Project:
Background
Origins of the PRL Project
The PRL research group was founded in 1979 by Joseph L. Bates and Robert L. Constable. It began as a project to build a logic-based program development system in which programs are constructed by interactive refinement. It combined ideas of Bates on program development by refinement with those of Constable on the design and automation of programming logics.
The Nuprl Systems
Since 1984 the project has been concerned with a particular family of proof development systems (also called provers or verifiers or logical programming environments or problem solving environments). These systems realize our ideas on program development, programming logics, automated deduction, logic, foundations of computer science, formal methods, and programming languages and their environments. They have all been called Nuprl (pronounced "new pearl") which are instances (instance Greek "nu") of what we now call a Proof Refinement Logic (PRL).
The identifiable versions have been Nuprl 1, Nuprl 3, Nuprl 4 and Nuprl 5 aka FDL (FDL is an acronym for Formal Digital Library)
Applications
The technology that we have already deployed in Nuprl 4 is being applied to improve the reliability of real world software systems. In a joint project at Cornell with Ken Birman's distributed systems group, we have helped verify components of the Ensemble group communications system. (Citation.) We have developed a methodology that we call hardening of software that uses Nuprl to incrementally verify properties of software systems.
At Bell Labs the HOL/Nuprl system created by Howe and Felty is being used in the verification of the SCI cache coherency protocol.
We have experience in applying Nuprl to engineering problems from the work of Aagaard and Leeser in EE who used the system to verify circuits and CAD tools.
Dynamics of the Project
Connections among these aspects of the project offer an interesting slice of computer science research dynamics. We see theory "at work" as it informs design and as it clears away technical roadblocks. We see applications as they stress the software and the methodology. We feel the impact of external technology such a fast processors, large disks, expressive programming languages and the Internet. The increased power and decreasing cost of hardware has fueled our progress and widened our horizons.
The interplay between these aspects of the project offers an interesting view of computer science research. One can see the role of theory as it informs our designs and is marshalled to overcome technical problems. This is apparent in the narratives about each area in which we see system design guided by results in Logic and Theory. We see the implementation problems posing new challenges to the theory. We also see that foundational design decisions impact every layer of work built on top.
We also see the role of applications in stressing the system, determining priorities and dictating the kind of mathematics that is formalized. We see advances in Programming Languages having a steady influence on our tools and implementations. Conversely, our formal methodology feeds into programming language design and methodology. Likewise, advances in Systems require us to constantly reimplement parts of Nuprl to achieve concurrency, to achieve modularity, to achieve portability. In this area our work on applications of Nuprl to the Ensemble group communication system turns out to provide us with a more secure communications substrate, part of a large effort to harden Nuprl in the sense of making it more reliable and safe.
One of the new phenomena resulting from the project's longevity is that we have built a large data base of formal mathematics. Managing this has led us to study database transaction mechanisms and study retrieval techniques that can be automated in the proof tactics.
Why link logic-based tools to support programming with implementing formal computational mathematics?
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.