Here are contributions, made after the workshop ended, explaining major ITP systems' approaches to trust. ---------- Isabelle ---------- Larry Paulson (with feedback from Burkhart Wolff): Isabelle uses the LCF approach to soundness. There is a proof kernel although somewhat larger than that of a typical HOL system because it includes an implementation of higher-order unification. Isabelle can generate full proof terms that can be checked independently, although it normally generates minimal proof terms in order to save space. External reasoners can be used as trusted oracles, but all such uses are labelled as such in the proof term even if minimum terms are enabled. Isabelle includes computational reflection, and the results of computations can be accepted as theorems. This involves trusting about 2000 lines of code that describes how to translate executable fragments of higher-order logic into one of several functional programming languages. Of course, the corresponding language implementation must also be trusted. Isabelle proofs do not generate theorems from such computations unless the user asks for this explicitly, and such theorems are always labelled as coming from an oracle. ---------- ACL2 ---------- Matt Kaufmann and J Moore: The ACL2 code base consists of approximately 240,000 lines of code -- 10.5 MB -- as of July, 2010. There is no subset identified as a ``trusted'' code base. While more than 1/6 of the lines are comment lines, and the source code also contains documentation strings (generating more than 1700 pages if printed), nevertheless this is a large base of code to trust. Trust thus rests on the two individuals who maintain the system, who apply their experience (over 70 years combined in logic and automated reasoning) and passion towards producing a system that follows its careful logical foundations (see http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html#Foundations). Users can extend the power of the system, but only (if the two system maintainers have done their job well) in ways that respect its foundations. Such extension facilities include a definitional principle, introduction of (witnessed) constrained functions, and a powerful but safe macro facility. Many trustworthy features are provided to extend the behavior of the automatic theorem prover, including use of previously proved theorems as rules of various sorts, reflection principles, and both static and computed hints. Computation is used during proof. Users have the power to connect to external tools (see for example http://www.cs.utexas.edu/users/sandip/publications/clauseprocessors/main.html), or even to subvert the system, provided they employ trackable ``trust tags'' that must be made explicit when verifying (``certifying'') a collection of input files (``books''). For maximum trust, ACL2 users should certify all books of a proof development, in an environment without other processes writing to the ACL2 or user space in the file system, and either without the use of trust tags or with explicit inspection of their uses. ---------- ProofPower ---------- Rob Arthan: For the record, the ProofPower trust story is the LCF story, backed up by a formal specification (but no proof) of the HOL language, logic and critical properties of a proof tool. The support for Z in ProofPower is an example of an extension in the sense of a semantic embedding of a new object language with a trust story piggy-backing on the trust story of ProofPower-HOL. The trust story for both ProofPower-HOL and ProofPower-Z includes the fact that the system is interactively programmable, so an evaluator who wants to can really dig in and pick syntax to pieces, which, in principle, mitigates the risk of problems of the sort recently discussed in Freek Wiedijk's (somewhat light-hearted) paper on what he calls "Pollack Consistency" see http://www.floc-conference.org/UITP-program-day195.html. In practice, the fact that you can easily code up things like reports on which definitions have been proved consistent and which have been given as axioms seems to be appreciated by commercial users. (Evaluators really like checklists!). ---------- HOL-4 ---------- Konrad Slind: HOL-4 is an implementation of the so-called LCF style, in which an abstract datatype is used to implement the primitive rules of inference of a logic, higher order logic (HOL) in this case. On top of this kernel, arbitrary ML programming by arbitrarily naive users may be used to construct theorems. If the kernel is a correct implementation, only genuine HOL theorems may thereby result. The kernel is small enough that its correctness may be established by inspection, informal proof, or even formal proof. Interface with external proof tools is usually performed by translating witnesses provided by the external tool into HOL proofs, which are replayed through the HOL kernel, obtaining the desired proof. However, occasionally it is convenient to directly accept the judgement of an external tool. In those cases, one can create a "tagged" theorem, where the tag designates the external tool. Tags accumulate through primitive inference steps, with the result that if a theorem th1 is obtained by primitive inference on a tagged theorem th, then th1 also becomes tagged. Consequently, only a theorem without a tag can be truly said to have been obtained purely by HOL inference steps. HOL-4 provides "persistent theories", in which the results of a theory development can be cached on disk, in a readable format. Since the disk representation of a theory can be maliciously edited, tags are also attached to definitions and theorems imported from a persistent theory. In summary, one way to believe that a claimed theorem in HOL-4 has a formal proof in the HOL logic is to do the following: 1. Arrange all theories needed to prove the theorem in dependency order; 2. Execute the theories, one at a time, in a single session (to avoid using persistence); 3. Check that the theorem of interest is indeed proved, and also check that it has no tags attached. Another way to believe that a claimed theorem in HOL-4 has a formal proof is to check a proof object created by a run of HOL-4. Some argue that checking such proof objects provides a stronger level of trust than an LCF-style kernel. Code supporting the generation and checking of proof objects has been implemented several times for HOL-4 but its use is not yet commonplace. ---------- PVS ---------- Natarajan Shankar: PVS is primarily a research platform for experimenting with different modes of inference, the interaction between formal language and inference, as well as issues of trust and automation. Trust in PVS is not merely a matter of ensuring that the inference steps have been correctly implemented. PVS provides an expressive language for capturing mathematical concepts directly and precisely. The automation available in the form of typechecking and theorem proving is directed at making it easy to construct, debug, verify, and maintain proofs. The PVS specification language is based on a higher-order logic enhanced with predicate subtypes, structural subtypes, dependent types, parametric theories, theory interpretations, and algebraic and coalgebraic datatypes. Typechecking a PVS expression generates proof obligations. These must be proved in order for the expression to be considered well-formed. Subtyping in PVS rules out undefined function applications, division by zero, out-of-bounds array accesses and updates, and misapplied datatype accessors. Theory interpretations can be used to instantiate abstract theories as well as to exhibit models of axiomatic theories. A large fragment of the PVS language is executable. The type system and operational semantics ensure that the execution of a well-typed PVS expression in this fragment cannot trigger a runtime error (other than by exceeding resource limits). The PVS proof engine is built from a small set of primitive inference steps. Most of the inference steps are small, but a few involve deep combinations of decision procedures and rewriting. Larger proof strategies can be defined using the primitive ones. Several external proof tools for BDD-based simplification and model checking, monadic second-order reasoning, nonlinear arithmetic, and predicate abstraction have been added to PVS. These external tools are trusted, but the code used in defining strategies need not be trusted since the proofs can be expanded down to the primitive inference steps. ---------- Coq ---------- Laurent Thery: Following Curry-Howard's isomorphism, Coq logic is based on a typed lambda-calculus: the Calculus of Inductive Construction where propositions as seen as types and proofs as programs. Its trusted computing base consists in its typechecker only: it is the piece of code that asserts that a given program has a given type, i.e. that the program is a proof of the corresponding proposition. If each proved proposition in Coq comes along with its associated proof-object, this object is not a simple recording of all the primitive logical rules necessary to get to the proof. Because proof-objects are really programs, they may also include computations. This makes it possible to have explicit proof-objects even for large applications. In particular, most of the trusted extensions that have been developed within Coq uses this capability of replacing proof steps by computations. This is the so-called computational reflection[1]. A call to an external tool is then represented in proof-objects by a call to a certified checker that verifies the certificates or the traces that are generated by this external tools. [1] Stuart F. Allen, Robert L. Constable, Douglas J. Howe and William E. Aitken, The Semantics of Reflected Proof, LICS 1990.