Skip to main content
PRL Project

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.