Building Proof Assistants
Build proof assistants that are as indispensible 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 indespensible 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.