20
$\begingroup$

Background

In my personal experience, the biggest bottleneck to broader adoption of proof assistants (in industry and mathematics) is the effort it takes to engineer proofs. (In lines of code, for example, verification of software often has 10x--100x as many lines of proof as lines of code being verified.) I've found that one of the biggest bottlenecks in proof engineering is the performance of the proof assistant itself, to the extent that most of my PhD work could be described as "working around performance bottlenecks in Coq". (See also my thesis, "Performance Engineering of Proof-Based Software Systems at Scale".)

Question

What is known about performance bottlenecks in proof assistants and automated theorem provers?

I'm especially interested in two sorts of answers:

  1. Existing knowledge about best practices and performance trade-offs in implementing proof assistants (e.g., tradeoffs of term representations, tradeoffs of unification variable representations, state-of-the-art algorithms for performant reduction, type inference, typeclass resolution, etc)
  2. Personal experiences of performance bottlenecks in using proof assistants, and tips, tricks, and knowledge about what causes them and how to diagnose and work around them.
Improve this question
$\endgroup$
5

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Browse other questions tagged or ask your own question.