I define *Proof Engineering*
to mean the activity of construction, maintenance,
documentation and presentation of large formal proof
developments.

Proof Engineering will combine the best of software engineering with the best of computer-checked formal proof: Software Engineering provides the techniques to develop large, structured and well-specified repositories of computer code; proof checking provides the mechanisms to provide a complete semantics and formal correctness as an absolute quality criterion.

Since the early 2000s onwards we have witnessed some
truly **heroic** efforts in large scale mathematical proof and
formal verification, such as the
Flyspeck
project in which Thomas Hales led construction of a formal version of
his proof of the Kepler Conjecture;
the Proof of the Feit-Thompson Theorem led by Georges Gonthier;
or the verification of security and safety properties of the
seL4 Microkernel
led by Gerwin Klein.

These successes and others have relied in advances in the state-of-the-art in formal
verification methods and tools, but are still pioneering and far from
what can be easily achieved in ordinary timescales for informal mathematical
proof or typical program development. They been built in spite of the primitive nature
of the tools involved. While automation has improved, it could still
be much better and use smarter techniques to learn from previous proof development
attempts. And the development environments for formal proof,
which authors use to write and manipulate them, could be *made vastly* better,
including my beloved but *well*
past-its-sell-by-date Proof General
environment.

- Continuing towards rigorous foundations for Proof Engineering, Iain Whiteside completed his PhD on Refactoring Proofs in 2013, based on some simplified formal models of proof scripts inspired by the languages used in Isabelle and Coq. A paper from Iain's thesis won the MKM Best Paper Award in 2012.
- Outside Edinburgh, recent efforts at improved proof development environments include Isabelle/Eclipse and the CLIDE web interface which both use the PIDE framework, a design originated by Makarius Wenzel that mandates deep integration with the underlying theorem prover from the start. This enables sophistication such as background proof-checking and checking that prioritises where the user is working, or "IntelliSense" style interactive help, features that Wenzel has been steadily implementing in the Isabelle/jEdit primary Isabelle interface.
- In late 2000s, I started a collaboration with
Ewen Denney and
Christoph
Lüth on rigorous foundations for proof development, by
examining the objects of the development process (not just the proofs
and logical systems). This line of work builds on Ewen's notion of
*hiproof*, which adds*hierarchy*as a primitive form that can be used to give navigable structure to proofs or proof scripts. This line of work has has been theory-first so far, with only experimental prototypes. - In 2005-8, Daniel Winterstein, Alex Heneveld and David Aspinall developed an Eclipse-based version of Proof General. It was a fragile first effort and (as typical with Eclipse plugins) difficult to maintain, but gave some hints of what a sophisticated IDE could bring to proof development.
- Although Proof General is still used by many, we realised its limitations years ago. In 2002-5, together with Christoph Lüth, I designed an abstracted version of the Proof General interaction protocol and a middleware layer called Proof General Kit which enabled more sophisticated operations. One criterion was to be a minimal burden to theorem prover developers: we viewed changing the theorem prover as difficult or impossible (in case of closed source), and it was hard to motivate to theorem prover developers who tended to be more interested in the underlying logic foundations or proof procedures than interfaces. We relaunched the UITP workshop series but usability seemed like a far off concern for most.

Contact GPG key (Instant HOWTO)