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

Papers and talks

coming soon

my Vcard
David R. Aspinall, email
Contact GPG key (Instant HOWTO)