Proof Engineering
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.
Making formal proof less heroic
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.
Our work so far
Under construction
- 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.
Papers and talks
coming soon
