Our approach to the problems enumerated above is based on years of experience with the cycle of designing and building a verification system based on the latest advances in theory, experimenting with it on real problems, distilling insights and results into new theory and new designs and repeating the process.
This process has convinced us that a programming environment based on a real programming language at its core is the way to tie verifications to running code. The latest success from this approach is our ability to verify the stack compression technique used in the Ensemble group communications system.
Another significant insight that drives this proposal is that we know how to combine the verification systems HOL and Nuprl to the extent that they can share a common data base of facts. We judge this to be a significant advance illustrated by the preliminary results using the system []. Our experience with this prototype convinces us that we can at least add facts proved by PVS. But much more seems possible as we outline in B3 and B4.
The additional capabilities derive from our work with the Nuprl library mechanism. We know how to keep track of logical dependencies between theories using proof sentinels. and thus how to create proofs whose inference steps can be done by different systems. Moreover, we have designed and tested a general module mechanism for relating theories that is the basis for extending the HOL/Nuprl prototype. The module system will also help us attack the problem of creating verified light-weight tools as we describe in below.