Mission Statement
Proof General Developers
March 2000
We seek to provide an interface suite for helping users interact with
proof assistants.
Our approach is based on these principles:
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
.