FOM: Re: Re: Godel, f.o.m.

[charles silver]

    Thanks for the reference to the Barwise article.  I'll try to locate it.

Steve Stevenson:
>... I think a far more interesting question
>for computing is not the universal-ganzenmacher algorithm and the
>once-and-for-all (since we can't do it). I'd rather concentrate on
>what I can do. I'll repeat something that I heard but can't properly
>attribute but it was bW [before Wiles]: "No one cares about Fermat's
>Last Theorem because nothing hinges on it. But we care about the proof
>since that will tell us volumes."  I find myself taking on a position
>that I cannot win in this forum. Mathematics is not always a
>meaningless bunch of symbols being pushed around. For those people who
>use mathematics to solve problems in their disciplines (like physics,
>chemistry, and engineering), the question is "How reliable is your
>mathematics?" Think about it the next time you fly, 'cause the plane
>is being landed by computers, not humans.


    I don't get what you're saying in most of the above, but I'll pick out a
couple of sentences and offer a few reactions.   Regarding: "I'd rather
concentrate on
what I can do," I have to admit I've had the experience of trying to verify
a very simple computer program and failing over and over again, and finally
realizing that the "very simple" program I was trying to verify was just
plain wrong.  So, from this meager experience, I have to say that, despite
the many problems associated with program verification, I found that it can
be valuable.   I'm not trying to dismiss your points about not leaning too
much on program verification.  All I'm claiming is that in some cases it can
be helpful.   As you might say, "it's a tool."

    Specifically, I'm not sure why you say "the question is 'How reliable is
your
mathematics?' Think about it the next time you fly, 'cause the plane
is being landed by computers, not humans."   I think I'm probably being
dense here, but I don't get it.   Isn't the math absolutely knock-down
reliable, in Descartes's sense (meaning: you can't doubt it)?  But, I don't
think it's the *math* that's in question (is it?).  Isn't the question
whether you can be *certain* you haven't made a mathematical error when
verifying a program?  If you're saying that I may not be comfortable with
simply verifying a computer program that lands a plane, you are absolutely
right!  I wouldn't want to rely simply on the result of a verification.  One
thing I'm wondering about is how *often* a program is verified and wrong.
That is, does anyone know how often mistaken verification *actually* takes
place?  My guess is, not often, though I concede that it *can* happen.

    I have the feeling you are arguing against a brand of Formalism.  If I
am a Formalist, I don't realize it.  Not long ago, I had a big argument with
a Formalist, so if I really am one, I owe him an apology.

>Charlie, we're looking at this from different perspectives and so will
>never quite come to grips with the whole thing.

    Well, I think our differences are more of degree than of kind.  I tend
to think program verification is a useful tool, though I concede that it's
not the be-all and end-all some people think.


> My view of mathematics
>(and computer science) is this: is it part of the solution space or is
>it part of the problem space? If it's part of the solution space, then
>how reliable are the judgements I must draw from using it when it
>comes down to building real <anything>?


    I think of math as being more useful as backup in this context, and less
useful in the *creation* of something new.   But, I may again be missing
your point.

Charlie