| 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.
|
