Nuprl is a large computer system. We sometimes think of it as a "logical operating system" because it must perform many of the tasks of an operating system but in a logically correct manner. For instance, the library is like the file system, but it must account for truth. It is transaction based, so there are primitives for locking sections of the library. The proof engine or refiner can create processes that run concurrently, but their results must be linked in a logically sound manner. Nuprl processes communicate among themselves and with external processes, so Nuprl must manage concurrent processes.
Nuprl runs on three different operating systems. We learn the technology for building it from our colleagues, but we have also made some contributions which are usually buried in our papers on other topics. These are related to our contributions to Software Engineering.
The systems component of our work is also a major challenge to our theory. We would like to reason about the Nuprl system as well as about the Nuprl logic. To do this we need a theory of processes and events that is more fundamental than the current models that we use applications. For some time this will remain a challenge.
One of the basic systems concepts contributed by our implementation is Stuart Allen's idea of a "working map" as refined and implemented by Richard Eaton.