[FOM] Formal verification

[Lucas Kruijswijk]

Dear All,

To get to an older question of Lasse Rempe:
> I would be interested to know what, in the view of those who know about the current state of things, is the main current obstacle to a wider use of computer verification in the medium term (say the next 10 years):
>  
> a) Competing systems and paradigms in the formal proof community;
> b) Lack of engagement from ‘mainstream’ research mathematicians;
> c) Lack of funding;
> d) Some fundamental issues on a theoretical level that still need to be overcome?
I would like to add one thing that has not been mentioned in recent posts and which is not
in above list.

To get more formal and computer verified mathematics, I think we should take a look at the education.

I will illustrate this with my own experience. I am a computer scientist with an interest in logic. So, my
knowledge is somewhat limited (but I am motivated!).

When I took some courses in logic as part of my study in computer science (more than 20 years ago),
I didn't get any lessons how to write a fully formalized proof. And if I look at the current student material
now, I don't see much change (but I only checked a few sources). If you buy a book about introduction
of logic, you don't get any hints how to really do mathematics formally.

At a certain point I even thought that fully formalized mathematics was still "an unsolved problem".
And I do think that many scientist that didn't specialize in logic or mathematics do think the same.
This idea might be unconsciously fed by Gödels incompleteness theory. The advertisement of
Logic is very bad, we emphasize that things can't be done, rather that things can be done.

Only after I finished my study and started to look further, I got some ideas how to do math in a
formal way. The best source were the manuals of the different provers. This was still hard. 

So, I think education should change. Logic is not like mathematics. Logic evolves while mathematics
only grows. With the introduction of the computer, the ideas about logic got subtle changes, but we
didn't change the education.

Learning the skill of formal math in first courses in Logic would require that other subjects need
to be moved to advanced courses. I do think that is the case with models. I don't see why 
someone that doesn't continue with Logic needs to learn that.

For more formal math I think the two sides must grow to each other:
- The informal proofs must be written in such a way that they can easily formalized, easier than
  current practice.
- The provers must become closer to current (written) mathematics.  

With the proposed education a new generation will be bred, that will advance on both sides.

Taking into account above argument I think without change in education formal math, verified
by computer will not become mainstream.

Regards,

Lucas Kruijswijk

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20141028/021a13ce/attachment.html>