Static and User-Extensible Proof Checking
Despite recent successes, large-scale proof development within proof assistants remains an arcane art that is extremely time-consuming. The authors 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, they rely on developing and using tactics, specialized procedures that produce proofs.