[FOM] Formal verification

[Freek Wiedijk]

Hi Lasse,

>a) Competing systems and paradigms in the formal proof community;

The two competing families of systems are type theory and the
HOL systems, with Coq versus Isabelle on both sides being
the dominant systems.  Both are _very_ different.  If you
want classical math (the math of "'mainstream' research
mathematicians" :-)) then Coq (even with HoTT) is not very
attractive.  If you want dependent types (and you want that)
then Isabelle is not very attractive.  What would a good
synthesis between Coq and Isabelle look like?  I don't know.

>b) Lack of engagement from 'mainstream' research mathematicians;

Maybe.  It would help if it became clear whether these
people consider it important to have full classical ZFC
available or not (i.e., whether they don't mind working in
the formal world of Bishop's mathematics, where you cannot
prove the intermediate value theorem if you state it the
naive way, say.)

>c) Lack of funding;

Maybe.  (I'll not say "No" to this one :-))

>d) Some fundamental issues on a theoretical level that still need to be overcome?

No.

You forgot the main reason:

e) Lack of good automation.

Currently doing formal proof goes too slowly to be really
pleasant.  The hammers -- like Isabelle's Sledgehammer --
help, but maybe not enough yet.  You still need to be aware
of a lot of details that you normally would leave implicit.
At least, I think.

Freek