Building systems in proof assistants is challenging for many reasons. Such systems must tolerate changes gracefully: definitions may be optimized for performance, new theorems may be added, and the proof assistant itself may change how tactics work. Proof assistants are also highly expressive; engineers must ensure that their specifications do not accidentally allow for undesirable behavior. Furthermore, large-scale developments often depend on good tactic performance, requiring developers to reason about low-level performance costs.
To help address these challenges, the Proof Engineering (PE) project is collecting best practices for developing large systems in the demanding and foundational context of proof assistants.
May 2017 Site goes live.
Our first effort is assembling a survey of existing proof engineering work.
ProofEngineering is an international collaboration between researchers at the University of Washington, University College London, and the University of Illinois. Many volunteers have helped out on PE projects; we're very grateful for their contributions! Folks currently working on PE include: