Return to Answer

http://www.proof-technologies.com/holzero.html

http://www.proof-technologies.com/holzero

A) The LCF-style kernel is not as purely implemented as may be expected. Some systems have back doors to creating "proved theorems", such as importing the statements (but not the proofs) of previously proved results from disk, and trust that the user will not abuse this. Also, to reduce execution time, various derivable inference rules are implemented as primitives, multiplying up the size of the trusted source code. Also, the kernels typically incorporate large amounts of supporting code (e.g. for organising theories) and are not particularly clearly implemented, and so are difficult to review. It should be noted that HOL Light does not suffer from any of these problems.

I have developed an open source theorem prover called HOL Zero, that addresses issues A-C listed above and is designed for use in proof auditing and to be as trustworthy as possible. It has a watertight kernel, a robust pretty printer and the source code aims to be as clear and well-commented as possible. However, it does not have the advanced automatic and/or interactive proof facilities of the existing systems I list above, and is not suited to developing large formal proofs. HOL Zero can be downloaded from here (it needs OCaml and a Unix-like operating system):

A) Most "LCF-style" systems do not implement the LCF-style kernel idea as purely as may be expected. Some systems have back doors to creating "proved theorems", such as importing the statements (but not the proofs) of previously proved results from disk, and trust that the user will not abuse this. Also, to reduce execution time, most systems implement various derivable inference rules as primitives, multiplying up the size of the trusted source code. Also, the kernels of most systems typically incorporate large amounts of supporting code (e.g. for organising theories) and are not particularly clearly implemented, and so are difficult to review. It should be noted that HOL Light does not suffer from any of these problems.

I have developed an open source theorem prover called HOL Zero, that addresses issues A-C above and is designed for use in proof auditing and generally to be as trustworthy as possible. It has a watertight inference kernel, a well-designed concrete syntax and pretty printer, and the source code aims to be as clear and well-commented as possible. However, it should be noted that it does not have the advanced automatic and/or interactive proof facilities of the existing systems I mention above, and is not suited to developing large formal proofs. HOL Zero can be downloaded from here (it needs OCaml and a Unix-like operating system):

B) The trusted source code in LCF-style systems is NOT limited to the LCF-style kernel. Like in all systems, it at least also includes the pretty printer, since, in practice, the user will only view results displayed via the pretty printer. However, each system has problems with its pretty printer that allows misleading information to be displayed to the user (e.g. by using irregular variables names, or names that are overloaded). I have found many ways of appearing to prove "false" in these systems! Also, depending on how the system is used, the parser is arguably also a trusted component.

B) The trusted aspects of an LCF-style system is NOT limited to the design/implementation of its LCF-style kernel. Like in all systems, it at least also includes the design of the concrete syntax and the implementation of the pretty printer, since, in practice, the user will only view results displayed in concrete syntax via the pretty printer. However, each system has problems with its concrete syntax and/or pretty printer that allows misleading information to be displayed to the user (e.g. by using irregular variables names, or names that are overloaded). I have found many ways of appearing to prove "false" in these systems! Also, depending on how the system is used, the parser is arguably also a trusted component.