From 670761dd6bd6321d65beeacdc81d68c0a2ebe92b Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Mon, 13 Mar 2000 05:14:23 +0000 Subject: Updated web pages. --- html/mission.phtml | 138 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 138 insertions(+) create mode 100644 html/mission.phtml (limited to 'html/mission.phtml') diff --git a/html/mission.phtml b/html/mission.phtml new file mode 100644 index 00000000..00f7b60f --- /dev/null +++ b/html/mission.phtml @@ -0,0 +1,138 @@ + + +
+

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, rather than +to provide publications by conducting research in +human-computer interaction. +

+

+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 +. +
+
+ + + -- cgit v1.2.3