[FOM] Adventures in Formalization

[Natarajan Shankar]

Dear Harvey: I read your FOM postings on ``Adventures in Formalization'' 
with interest, and
sympathize with the spirit of your remarks and quite a few of the 
details.  Here's some
feedback on the Beautiful Formalization Project (BFP) from the 
perspective of our
PVS proof assistant whose design goals closely match several of the 
criteria that you have outlined.

By way of background, for at least thirty years now, it has been the 
case that most of the
proofs from the mathematical literature prior to 1950, say, have not 
been particularly
challenging to machine-check even for proof assistants with fairly weak 
automation.  There
are several substantive proof libraries that would enlighten your 
``typical skeptical
mathematician''.  The more interesting challenge is to construct 
formalizations that are
beautiful, so that even the ``nuanced doubters'' are convinced that 
there is good value to
be derived from the formalization process and the availability of formal 
mathematical
content supported by powerful inference algorithms.

THEOREM STATEMENTS: You are indeed correct in asserting that the 
readability of the formal
presentation is critical.  This is especially the case in computing 
where many errors lurk
in the formalization of informal ``requirements''.  On this dimension, 
formal mathematics
with mechanization can go considerably beyond informal mathematics to 
support a precise yet
natural mathematical vernacular.  As a simple example, I always took it 
on faith, as
virtually every textbook treatment does, that (n choose k) = n! 
/k!(n-k)! defines an
integer.  It helps to have a typechecker tell you that this isn't 
entirely obvious, and
that furthermore k should be at most n, and that the division is fine 
because the product
of two factorials is never zero.  (Free logics of the kind you suggest 
turn out to be quite
a bit more painful than clearly restricting the domain of the 
denominator to nonzero
numbers.)

ABSOLUTE INFALLIBILITY: As Paulson already mentioned, there already are 
some quite impressive
attempts to shrink the trusted core.  More below.

GOLD STANDARD: Over the past few years, I have been working 
intermittently on a project
called the Kernel of Truth (KoT) to bridge the gap between a usable 
formal language with
efficient mechanized inference and a small trusted kernel for exactly 
the kind of core
logics you have in mind.  The premise of the project is that a typical 
proof engineer
wishes to work on a domain-friendly formalism with domain-friendly 
automation that might be
untrusted and even experimental.  Typically, a lot of this proof work is 
exploratory but
every now and then, claims need to be certified.  For this, the 
untrusted proof engines
generate certificates and these certificate/claim pairs are checked 
using checkers that
have been verified relative to the trusted kernel.  This way the 
certificates need not be
expanded down to proofs at the kernel level, as is the case in the LCF 
approach. Also,
certificate checkers are considerably easier to verify than your typical 
SAT/SMT solver.

SELF PROVING: This was a hugely important design consideration in PVS 
when we were
developing the system twenty five years ago.  Many features of the type 
system work
effectively only when there is adequate automation for the trivial 
inference steps.  We
wanted proofs to be developed through a dialogue at roughly the same 
level of detail and
proof hints as a convincing informal exposition.  Trivial inference 
steps and
simplifications should be handled by decision procedures for 
propositional logic, equality
reasoning, and for theory combinations including linear arithmetic. Most 
of the time is
spent on exploratory proof attempts that fail, and they fail because 
either the statement
is unprovable or the proof is incorrect.  We therefore tried to use the 
automation to
simplify the statement to a point where the error is apparent. Overall, 
the user guides
the proof by suggesting induction, non-obvious/non-local case splits, 
lemmas, and
instantiations.  The proof dialogue is based on HAVE/WANT-style sequents 
with user-supplied
proof hints that drive the proof goal into easily decidable subgoals.  
However, obviousness
can be a moving target.  For example, the first couple of cases in a 
proof could be
nontrivial, but the remaining cases may not hold any new surprises. 
There is plenty of
scope for improving the automation to expand the range of obvious 
inferences, particularly
to cover obvious inferences involving quantifier instantiation and 
nonlinear arithmetic
equality and inequality constraints.

In summary, modern proof assistants have experimented with many ideas 
that are similar to
the ones you have proposed and there is a large body of accumulated 
evidence that can
definitely inform your thinking on BFP.  Conversely, it would be great 
to have your
feedback pinpointing opportunities for radical improvements.

Best regards,
Shankar