I have some thoughts about how to design a proof verifier, and want to get feedback (eg why existing systems don’t do things this way, or if there are some that do).
LCF-style proof systems generally have a small logical kernel, which they build on to add tactics. However, the kernel is still deeply integrated into some larger tool, often with subtle back doors for performance reasons. I would ideally like that kernel to be a separate program accepting low level proof steps as input in some clearly specified format, and outputting just enough information to indicate what has been successfully proven. Thus, having audited the verifier, one could feed an arbitrary proving program into it and trust the result. I see the following advantages of this separation:
- Forces a clear boundary and interface on the verifier, making it easier to audit.
- The proof can be trivially extracted as data for other purposes, eg ML training.
- Multiple verifier implementations could be cross-checked against each other.
- Provers could be implemented independently of the verifier for various proof methods, such as:
- Replay a stored proof
- Generate low level proof steps from higher level tactics
- Run an algorithm generating a proof of a specific computational result (the kind of case that would warrant a Coq plugin)
- Feed steps from an AI model
- Apply a (possibly partial) translation from a different logical system
- A combination of the above
IIUC coqchk is a standalone verifier tool, but the .vo files it accepts are only understood by Coq tools, not in a well-specified format that other tools could produce or consume (see here). The closest existing tool I found is metamath0, but it leaves the proof format unspecified (up to the implementation).
For output, the verifier would:
- Tell the reader how to interpret any introduced notation (eg
x,y:nat |- x+y:nat). - Output theorems when requested by the prover (ie the prover can choose to hide intermediate theorems)
For definitions, the reader needs to be convinced that each symbol has its usual meaning. However, the most convenient definition for proof purposes may not be the simplest to understand. See this user comment: “I don’t want to dig through a particular construction of the reals from rationals to make sure that this is indeed the reals that I know.” Therefore the verifier would not show definitions. Instead, the prover would need to output theorems sufficient to characterize each symbol. Of course, one option is to simply output the definition as a theorem.