[FOM] Formal verification

[Freek Wiedijk]

Dear Bill,

>Again, our tidy souls (and mine) want foundations; but
>if you should ever be fortunate enough to have an Euler in
>your program, I bet you wont drive him/her away.

The fact that something is not for _everyone_ doesn't
seem a reason that it won't be interesting for _some?_
Let the creative minds be creative.  Let the people who
like things spotless try to be spotless, using the great
technologies that are currently available for that.  I don't
see the conflict.

As an analogy consider a nice vista, a sunset or something
like that.  Some people will enjoy that for its beauty by
just gazing at it.  But some people will take oil paint
and painstakingly make a painting of it, which will take
a lot of work and energy.  Why would those painters drive
the people away who just enjoy looking at that sunset?

Of course what we really would like to have in this analogy
is a photocamera :-)  (But for formal math that still has
to be invented, I think.)

Freek