Readers can evaluate the formal text on the Web that resulted from our formalization efforts. It is possible to directly judge whether our definitions are faithful to Hopcroft and Ullman's, whether the formal definitions help clarify the concepts, whether the proofs are sufficiently readable and informative, whether the availability of detail about all proof steps is useful and so forth. The formal material also provided the underpinning for this paper in that our definitions and proof summaries refer to the complete formal library. The material can be the foundation for other documents that explain the detailed proofs. We have not yet produced such documents for the automata library (but see the Conclusion), however, there are examples of this genre of writing in the Formal-Courseware section for the Nuprl home page. For example, Stuart Allen has produced a hybrid style of formal and informal proof to accompany that basic theorems about functions proved by Paul Jackson and used extensively in the formalization.
There are other aspects and by-products of our formalization that cannot be directly evaluated by reading the formal text; they require experience with the system. In this category is the experience of confidence in the results that comes from learning to trust Nuprl. We know that reading results checked by both a human and a machine raises confidence in their correctness, similar to the added confidence gained by having a trusted colleague check a result.
Another value of the formalization is the interactivity provided by the underlying system. Nuprl can show dependencies among theorems and definitions, and it can execute algorithms extracted from proofs. Users can modify proofs and see those effects on the execution, or try simpler proofs, etc.
In addition to the readable and highly interactive formal text, the formalization has created an interesting digital artifact, namely the formal theory becomes an object that we can manipulate, measure, transform and explore. To experience these capabilities, one must learn to use a system like Nuprl.