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

[Steve Stevenson]

charles silver writes:
 > >... 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."

I have the same experiences as you do with program verification. While 
there are some well known views and "foundations," we seem not to make 
much headway in this area. One of Dijkstra's famous "examples" is a
proof with predicate transformers on gcd. The problem with is "proof", 
as far as I can see, is that he reaches into a magic hat to pull out a 
number theory result that is true in the countable integers but
probably not true of finite integers in machines.

For the record, the two foundations I'm thinking of is Denotational
Semantics (Scott, Wand, Gougin...) and Axiomatic Semantics (Hoare, Dijkstra).

 > 
 > 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.

@article{social,
  author = "R. A. DeMillo and R. J. Lipton and A. J. Perlis",
  title = "Social Processes and Proofs of Theorems and Programs",
  journal = "Communications of the ACM",
  month = "May",
  year = "1979",
  volume = "22",
  number = "5"
}
More or less parroting the CS testing line from deMilo: Of the
thousands of proofs published every year, how many are without
error. I've heard numbers like 10% from reliable math sources.

 > 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.

Nope. I don't accuse anyone of being anything. I am trying to argue
for a more expansive view of mathematics and the role of computing
within mathematics. It gets used for something. I do not ascribe to
the point of view of Henry Smith:

"Mathematics: may it never be of any use to anyone!"

%I don't have any bibliographic info on Smith at hand, but I pulled the 
%following off the World Wide Web site for Math History at St. Andrews 
%University in Scotland:
%
%Smith, Henry John Stephen
%2 Nov 1826 - 9 Feb 1883
%Irish, lived in England
%His most important contributions are in number theory where he worked 
%on elementary divisors. He proved that any integer can be expressed as 
%the sum of 5 squares and as the sum of 7 squares.Eisenstein had proved 
%the result for 3 squares and Jacobi for 2, 4 and 6 squares. Smith also
%extended Gauss's theorem on real quadratic forms to complex quadratic 
%forms.
%Tommy Leavelle