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 requires 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.