The QED project will be a major scientific undertaking requiring the co-operation and effort of hundreds of deep mathematical minds, considerable ingenuity by many computer scientists, and broad support and leadership from research agencies.
Robert S. Boyer, "A mechanically proof-checked encyclopedia of mathematics: Should we build one? Can we?", CADE '94
[T]he following research questions would be interesting and beneficial to solve.
- What are the fundamental differences and similarities between proof engineering and software engineering?
- Can we estimate time and effort for a specific proof up front, and with which confidence? Related questions are: can we predict the size of the proof artefacts a project will produce? Are they related to effort? Can we predict the complexity or difficulty of a proof given artefacts that are available early in the project life cycle, such as initial specifications and/or code prototypes?
- Which technical tools known from traditional software development could make an even higher impact on proof engineering? Emerging prover IDEs for instance can provide more semantic information than typical programming IDEs, and refactoring tools can be more aggressive than their code counterparts because the result is easily checked.
- Are there more fundamental ways in which proof irrelevance, formal abstraction, and modularity can be exploited for the management of large scale proofs?
- Can concepts such as code complexity or technical debt be transferred to proofs in a useful way?
- Are there fundamental aspects of proof library design that are different to software libraries? What are the proof and specification patterns?
- Empirical software engineering has identified a number of "laws" that statistically apply to the development of large software projects. Which of these continue to hold for proofs? Are there new specific correlations that hold for large scale proofs?
Gerwin Klein, "Proof Engineering Considered Essential", FM '14
For the near future I see the need for more systematic tool support to maintain the growing repositories of formalized mathematics. There is also a need to make proof assistants more accessible to more users, to allow easy browsing and editing of such libraries.
Makarius Wenzel, "Interactive Theorem Provers from the perspective of Isabelle/Isar", In All about Proofs, Proofs for All, 2015
So, what needs to be done to improve proof assistant technology and make it more widely spread? According to me, we have to work on the following.
- Develop proof assistants further, working towards a simple basic technology that can be easily used. At this moment there are many different proof assistants. Basically, that is very good: competition leads to new ideas and improvement, by taking over and improving upon the ideas of others. Important points that need further development are: proof automatization and interfaces.
- Develop a joint platform for the exchange of ideas and mathematical content between proof assistant system and to the ‘outside world’ of interested scientists and users of mathematics.
- Big formalizations give feedback on the basis of those. The systems only get better if they are really used and their shortcoming are made explicit.
- Build up a basic library, where special care has to be taken of coherence, usefulness and documentation. To which extent is the library useful for a newbie who wants to formalize a theorem using the basic mathematical results of the library?
- Applications using the library. Can we use the proof assistant and its library when modelling and developing and verifying a new product, like a network protocol or the software operating a robot arm?
Herman Geuvers, "Proof assistants: History, ideas and future", In Sadhana, 2009
[I]t will take 140 man-years to create a good basic library for formal mathematics.
Freek Wiedijk, "Estimating the Cost of a Standard Library for a Mathematical Proof Checker"
I now do my mathematics with a proof assistant. I have a lot of wishes in terms of getting this proof assistant to work better, but at least I don't have to go home and worry about having made a mistake in my work. I know that if I did something, I did it, and I don't have to come back to it nor do I have to worry about my arguments being too complicated or about how to convince others that my arguments are correct. I can just trust the computer. There are many people in computer science who are contributing to our program, but most mathematicians still don't believe that it is a good idea. And I think that is very wrong.
Vladimir Voevodsky, "The Origins and Motivations of Univalent Foundations", In IAS Newsletter Summer 2014
It's all about economics. Given a piece of C code, we can choose to inspect it, to test it by hand, to fuzz it, to subject it to unsound static analysis, and to subject it to sound static analysis. Obviously, all of these validation techniques have merit - the question is how many resources to allocate to each of them. Larger, more rapidly evolving code bases tend to favor cheaper validation methods whereas smaller, security-critical codes are amenable to formal verification. The reach of formal verification techniques is increasing as techniques improve, but also software keeps getting bloatier.
John Regehr, "Comments on a Formal Verification of PolarSSL"
Sooner or later computer proof assistants will become the norm, but the longer this process takes the more misery associated with mistakes and with unnecessary self-verification the practitioners of the field will have to endure.
Vladimir Voevodsky, Univalent Foundations, Lecture at IAS, Princeton. Mar. 26, 2014.
Absolutely no technological barriers prevent the formalization of large parts of the mathematical corpus. The issues now are how to make the technology more efficient, cost effective, and user friendly.
Thomas C. Hales, "Developments in Formal Proofs", CoRR, 2014
As of early 2011, the under-development version of CompCert is the only compiler we have tested for which Csmith cannot find wrong-code errors. This is not for lack of trying: we have devoted about six CPU-years to the task. The apparent unbreakability of CompCert supports a strong argument that developing compiler optimizations within a proof framework, where safety checks are explicit and machine-checked, has tangible benefits for compiler users.
Yang et al., "Finding and Understanding Bugs in C Compilers", PLDI '11
[T]here is a lack of belief that [formal methods] scale - that [they are] worthwhile.
Bjoerner and Havelund, "40 Years of Formal Methods", FM '14
The tool support for formal methods is not sufficient for large scale use of these methods.
Bjoerner and Havelund, "40 Years of Formal Methods", FM '14
The programming language is becoming your specification language as well.
Bjoerner and Havelund, "40 Years of Formal Methods", FM '14
In truth, my motivations for the [Flyspeck] project are far more complex than a simple hope of removing residual doubt from the minds of a few referees. Indeed, I see formal methods as fundamental to the long-term growth of mathematics.
Hales, "Introduction to the Flyspeck Project", Dagstuhl Seminar Proceedings 05021
In the long run, formal verification efforts need better libraries of background mathematics, better means of sharing knowledge between the various proof systems, better automated support, better means of incorporating and verifying computation, better means of storing and searching for background facts, and better interfaces, allowing users to describe mathematical objects and their intended uses, and otherwise convey their mathematical expertise.
Avigad and Harrison, "Formally verified mathematics", Commun. ACM 57, 4 (April 2014), 66-75.