[FOM] Talk on Formal Verification

[Harvey Friedman]

I gave a general talk on formal verification, at

https://u.osu.edu/friedman.8/
downloadable lecture notes

64. Perspectives on Formal Verification, January 21, 2016, one hour
Keynote lecture, The Fifth International Conference On Certified
Programs And Proofs, St. Petersburg, Florida, delivered January 18,
2016, 11 pages.

This CPP meeting was a part of POPL, and I had several interesting
interactions.

While at the meeting, I firmed up some ideas for research on formal
verification of mathematical proofs, which may further our
understanding of the structure of mathematical proofs, even if it does
not provide any breakthrough in formal verification.

Most promising of my ideas at this point is the search for strong
uniformities in mathematical proofs.

If we go all the way down into the smallest steps in formal
mathematical proofs, we have complete - or largely complete -
uniformity across mathematical proofs.

If we look at bigger chunks than just these smallest steps, then this
uniformity begins to weaken or even disappear.

The plan is to uncover the right kind of small chunks that exhibit the
right kind of strong uniformity across mathematics.

This will require careful analysis and classification, along with
imaginative algorithms.

It may appear that a successful carrying out of such a program would
provide a breakthrough in formal verification of mathematical proofs.
However, there is a knotty program that is not directly touched by
this kind of program.

Specifically, suppose you have a large library of existing theorems.
When verifying these strategically chosen chunks in the proof being
formalized, one invariably is relying on some very tiny portion of the
library. The tiny portion of the library depends greatly on the
chunks.

I.e., all may be well and good if you know just what the relevant
items from the library are. But how are you going to locate these
items from the library?

There seems to be a lot of approaches to this library search problem,
but there needs to be a big new idea for it, in order for us to have a
breakthrough in the formal verification of mathematical theorems.

I conjecture that there is a powerful new way to construct libraries
that would make them more readily useful.

Harvey Friedman