We believe that the Nuprl formalizations of the Hopcroft and Ullman account of the Myhhill/Nerode theorem demonstrates the added value of formalization. The material we have created is a foundation for grounding informal explanations that refer to it for detail and precision. At Cornell we are experimenting with creating other examples of such formally-grounded explanations.
We have already formalized other parts of Hopcroft and Ullman, for example an account of grammars from Chapter 2 and nondeterministic automata. We judge that it would be possible to formalize Chapters 1-9 with our four person team in about eighteen months.
The collaboration methods we have learned would extend to larger teams. It would be especially interesting to collaborate with other theorem proving systems as Howe and his colleagues are doing with HOL and Nuprl [18][19]. Much of a classical treatment of languages can easily be re-interpreted constructively. It would be especially fruitful to collaborate with other constructive provers such as Alf, Coq and Lego or with Isabelle which has formalized Martin-Löf type theory. Although these provers are based on different formalizations of constructive mathematics, they all share the critical properties that computational notions can be expressed, and they all allow extraction of code from proofs.
With more work we could render our formal proofs as clear and readable as the informal ones. The simplest way to accomplish this is to reprove some results to improve their readability. Our experiments using the Nuprl editor to improve the readability of proofs has led to other devices we wish to explore such as structured presentation of tactics using our ML structure editor and the use of side proofs to further suppress detail and highlight the main thread of an argument. We are also following the work of the Centaur group to make proofs more readable [34][4], and we expect to use the modularity feature of the Nuprl-Light refiner [16] to help structure theories as part of a major effort to improve the readability of proofs.
Grant Support/Acknowledgments
We acknowledge the support
granted by the National Science Foundation and the Office of Naval Research. We also thank Stuart Allen and Karl Crary for the discussions and input concerning this topic and Karla Consroe for help in preparing the document.