A Role for Formal Methodists

Abstract

Proving “correctness” of entire systems is not now feasible, nor is it likely to become feasible in the foreseeable future. Establishing that a large system satisfies a non-trivial specification requires a large proof. Without mechanical support, building or checking such a proof is not practical. Even with mechanical support, designing a large proof is at least as difficult as designing a large program. We are barely up to the task of building large and complex systems that almost work; we are certainly not up to building such systems twice — once in a programming language and once in a logic — without any flaws at all.

This material is based on work supported in part by the Office of Naval Research under contract N00014-91-J-1219, the National Science Foundation under Grant No. CCR-8701103, and DARPA/NSF Grant No. CCR-9014363. Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the author and do not reflect the views of these agencies.