introduction › assistants

Building Proof Assistants

Build proof assistants that are as indispensable to programmers and mathematicians as word processors are now, by creating an environment in which:

• formalizing proofs will be as easy as writing Tex (also see Barendregt's goals);

• designing software will be guided by ease of formalization (also see Abrial's accomplishments);

• enforcing and monitoring design invariants will be automatic;

• developing, documenting and deploying code will be an order of magnitude easier (faster and cheaper) because it is done in a Logical Programming Environment.

Our strategy for providing such indespensable assistants is to build them as open systems that can import ideas and algorithms from the field of automated reasoning; that can connect to systems that provide symbolic computing services; and that can share libraries of formal mathematics with other proof assistants.