[FOM] Talk on Formal Verification

[Lawrence Paulson]

> On 22 Jan 2016, at 06:18, Harvey Friedman <hmflogic at gmail.com> wrote:
> 
> I gave a general talk on formal verification, at
> 
> https://u.osu.edu/friedman.8/
> downloadable lecture notes

Here is my attempt at answering some of the questions posed by this keynote lecture.

IS THE SIZE OF PURELY FORMAL PROOFS OBTAINED FROM
SEMIFORMAL PROOFS OF MAJOR THEOREMS REASONABLE? E.G., AT
MOST TEN THOUSAND PRINTED PAGES? OR IS THERE AN EXPONENTIAL
TYPE BLOWUP INVOLVED WHEN WE MOVE FROM THE USUAL SEMIFORMAL
PROOFS CREATED BY MATHEMATICIANS TO A FORMAL PROOF?

This is sometimes called the "de Bruijn factor”, after NG de Bruijn, who posed a similar question in relation to his AUTOMATH system. Generally the blowup is regarded as tolerable. For a specific example, I recently formalised the Stone-Weierstrass proof given here:

http://www.jstor.org/stable/2043993

The original is 3 ½ pages, including some nice explicit calculations. Even as someone who last studied such material 40 years ago, I didn’t have too many difficulties. The corresponding formal text in Isabelle is 579 lines or about 10 pages.

IS THE MENTAL EFFORT INVOLVED IN GOING FROM A FULLY
UNDERSTOOD SEMIFORMAL PROOF TO A FORMAL PROOF REASONABLE?

It very much depends on the subject matter. Where the intuitions are strongest, the effort of formalisation is the most frustrating. The Stone-Weierstrass proof above is a precisely laid out technical argument. But many obvious observations about finite sets, continuity, limits, etc need to be spelt out, sometimes at unreasonable length. In some cases, specialised automation could help.

HOW STABLE IS THE SIZE OF FORMALIZED PROOFS WHERE THE SAME
SEMIFORMAL PROOF IS BEING FORMALIZED WITH THE SAME SOFTWARE
BY DIFFERENT HUMANS? WHAT IF WE VARY THE SOFTWARE BEING
USED?

A more skilled and capable user will naturally find more direct and simpler proofs. The software is also critically important, because the length of a proof in terms of primitive inferences really is unbearable; the software has to provide plenty of automation so that only the creative steps are visible.

But a greater factor affecting the size is the subject matter. The use of meta-mathematical arguments can render formalisation difficult or impossible. (Sometimes however programming can be substituted, automating repetitive tasks in the proof assistant.) There are theoretical results stating that certain changes to the formal system can result in a non-elementary blowup in the lengths of proofs. A number of popular proof assistants use constructive mathematics, which can make things more complicated than their classical counterparts.

CREATE FORMALLY VERIFIED TREATMENTS OF VARIOUS BASIC AREAS
OF MATHEMATICS WHICH ARE SO READABLE THAT THEY CAN BE
EFFECTIVELY USED AS TEXTBOOKS WITH REAL WORLD NON COMPUTER
SCIENCE STUDENTS.

Readability of formalised mathematics remains a big problem. Much progress has been made on better notations for proofs, building on the structured proofs of the Mizar system (http://www.mizar.org). Mathematical formulas themselves are much more readable than before, but the need for an absolutely unambiguous syntax precludes innumerable well-known notational conventions.

THE MATHEMATICIANS WANT FREE LOGIC. 

A number of approaches to undefined terms have been tried, but as a rule they have not been popular with users. A very lightweight approach will have to be invented.

I WOULD LIKE TO SUGGEST A RELATED IDEA THAT SOUNDS VERY BOLD. WHY NOT TRY TO DECIDE ABSOLUTELY ANY INTERESTING CLASS OF MATHEMATICAL STATEMENTS, EVEN IF IT IS WELL KNOWN TO BE ALGORITHMICALLY UNDECIDABLE? HERE BY "DECIDE", I SIMPLY MEAN: PARAMETERIZE THE STATEMENTS IN QUESTION, AND START WITH VERY SMALL CHOICES OF PARAMETERS, CREATING MODEST SIZED FINITE SETS OF TARGET STATEMENTS. DEVELOP TOOLS TO HANDLE THESE EFFICIENTLY, AND THEN SLOWLY RAISE THE PARAMETERS, DEVELOPING MORE TOOLS, ETC.

This has been the approach to automation in Isabelle for 25 years, based on the common student observation that many problems can be solved simply by doing all obvious steps, combined with a small amount of trial and error. Isabelle’s automation can be supplied with theorems along with hints as to whether they should be regarded as obvious or non-obvious (the latter allowing search), and how they should be used. Compared with decision procedures, this approach has the great merit that it is almost always applicable and almost always makes progress.

WHAT DOES IT MEAN TO SAY THAT WE HAVE GIVEN A CORRECT STATEMENT OF A THEOREM?

That’s an excellent question, and my main worry when formalising anything. the system can check the proof that it can’t check the statement, apart from types, which give only a crude well-formedness test.

HOW CAN WE DESIGN THE ULTIMATE VERIFIER IN ORDER TO BE BEST SUBJECT TO VERIFICATION? 

In recent years, there has been much promising research in the use of proof assistants (especially HOL Light and HOL4) to verify their own kernels, and even to verify their translation into machine code. This is as high as standard as one could wish for. On the other hand, if we are demanding that these systems should be verified, it seems perverse to trust them for their own verification. Therefore we need the proofs to human-legible as well. They aren’t at all just now. But as somebody who uses such systems almost daily, I’d like to remark that confidence in such a system can be confirmed by its stubborn refusal to prove something in the presence of even the tiniest error in the set up.

Larry Paulson