Static and user-extensible proof checking

Despite recent successes, large-scale proof development within proof assistants remains an arcane art that is extremely timeconsuming. We argue that this can be attributed to two profound shortcomings in the architecture of modern proof assistants. The first is that proofs need to include a large amount of minute detail; this is due to the rigidity of the proof checking process, which cannot be extended with domain-specific knowledge. In order to avoid these details, we rely on developing and using tactics, specialized procedures that produce proofs. Unfortunately, tactics are both hard to write and hard to use, revealing the second shortcoming of modern proof assistants. This is because there is no static knowledge about their expected use and behavior. As has recently been demonstrated, languages that allow typesafe manipulation of proofs, like Beluga, Delphin and VeriML, can be used to partly mitigate this second issue, by assigning rich types to tactics. Still, the architectural...

• Type: Journal
• Year: 2012
• Where: POPL
• Authors: Antonis Stampoulis, Zhong Shao
• Keywords: Conversion Rule, POPL 2012, Programming Languages, Proof Assistants, Proof Scripts