Doing the work we propose will result in significant and interesting new capabilities. First, it will be possible to share results. It will be possible to use the appropriate logic engine for the task at hand and the appropriate logical theory. For example, a computational theory like Nuprl can talk about complexity constraints in its specifications. No other logic can do this, but in the LPE it will be possible to use this rich language. An indirect consequence of this accomplishment will be an incentive to share basic results that will motivate and enable other forms of cooperation.
In this section we comment on how the LPE will be useful in the on-going verifications at Cornell and Bell Labs. We also discuss how it will enable a broader use of the method of programming by extracting code from proofs. As Howe demonstrated, this capability can now benefit from theorems proved in noncomputational logics.