We seek to provide an interface suite for helping users interact with proof assistants.

Our approach is based on these principles:

• Be useful to both experts and novices.
• Be scalable to large proof developments.
• Be easy to learn, yet still provide advanced features.
• Be generic to support many proof assistants with a uniform interaction mechanism.
• Be a high-quality research prototype.

Above all, we take a pragmatic approach to constructing interfaces. Our primary aim is to provide a tool which is immediately useful for proof engineering.

This aim means that we harness a range of proven techniques reimplemented in our generic system. Nevertheless, by the act of constructing Proof General, we do invent and incorporate some novel advances which contribute to research in the field.

Footnotes and elaboration

Computer programs for constructing formal machine proofs. Terminology varies; we include all kinds of theorem proving systems which involve user interaction while a proof is constructed. We currently focus on systems based on a notion of proof script, which is a file containing a user-level representation of the proof or how it was constructed.

Many interfaces for proof assistants are aimed at novice or beginner users (and often used for teaching). Instead, we want to provide an interface which is useful for expert users in the first place. But we believe such a system can also be helpful for beginner users.

Some interfaces fail to scale to large proof developments; we want Proof General to be useful for real-life, large projects, consisting of many theorems and theories.

It is difficult enough to learn how to use the logic and language of a proof assistant, without an extra effort for learning its interface. We want to provide a friendly interface with intuitive features, hence a shallow learning curve.

Proof General is intended to be used with a variety of underlying proof assistants. We appreciate that different proof assistants are based on different logical principles, and implement different proof languages. Yet interaction between different systems often has a similar behaviour. We exploit this to provide a good user interface for many systems at once, saving repeated development effort by proof assistant implementors. It has the added benefit of providing a uniform interaction mechanism between different systems, making it easier for users to experiment with several proof assistants.

The developers are working on Proof General in the academic sector, and engineering work itself is not directly funded. Despite this, we strive to follow good engineering practices to build a robust and maintainable system, which users can easily install (or test on the web). To this end, we employ open-source development with frequent test releases before stable releases, and high-priority attention to user suggestions and bug reports. We use CVS for source control, a strategy of bottom-up successive improvement, and provide support for each proof assistant by an experienced user/developer.

Amongst other features, Proof General currently includes and , both championed in Projet CROAP.

Proof General also advances the state-of-the-art. For example, we introduced proof-by-pointing in an free-form environment, and extended script management to handle .