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

[charles silver]

> Vladimir Sazonov writes:
>  > <Snip Matt Insall's Comment>
>  > Here is not so much of contradiction because mathematics is just
>  > a kind of formal engineering. In a sense, computers as some
>  > (physically realized) formal systems belong to mathematics.


Steve Stevenson wrote:
> James Fetzer has a really great article on this particular view of
> computing.

    Geez, I remember thinking about 8 years ago when I read the article that
it had little content.   Wasn't the paper an extended argument against
program verification, and wasn't his main point just the standard Cartesian
criticism that we can always make a error, no matter how much we try to
verify a program with a formal proof?   The proof that the program is
correct may itself wrong, and other things can go wrong as well.  The reason
I thought his paper had little content--supposing I remember it
correctly--is that his argument seemed to apply to *everything*.  For
example, suppose I offer the following argument schema as valid in standard
logic:

        All A are B
        x is an A
_________________
Therefore: x is a B

And, suppose some large number of people--like the people in FOM--were to
examine the above schema and pronounce it correct.  It *could* be the case
that we're all mistaken.   It's *possible* for all of us to be wrong, even
in judging the validity of so simple an argument.  That is, it isn't
*necessarily* the case we can't make such a mistake.   But, I don't think
this overly general fact about our human fallibility has any  specific
importance to the proofs of program correctness.  That is, our fallibility
applies to *everything*, doesn't it?

>The gist of his article (please read it for all the other
> things) is what I have termed the Fetzer boundary. There is a point at
> which computing is no longer mathematics because it is no longer
> formal.


    Please correct me if I am wrong, but as I recall, his arguments apply
equally well to mathematics (except for his specific comments about
compilers, of course).  That is, consider a formal proof checker that's been
created to check the accuracy of math proofs.  It is possible for a proof to
be be wrong and for the proof checker to err (for any number of reasons) and
incorrectly label it as a good proof.  (And, if we thought we could shore
this up with a proof checker to check the proof checker, then *this* very
proof checker would need a proof checker, etc. etc.)  Again, this overly
general fact about fallibility doesn't seem to cut any ice about computer
science specifically.  Here, the Fetzer conclusion would be that math itself
is not formal, since one can't (in Descartes's sense) be *absolutely
certain* that a mistake in a math proof hasn't been made.

    (The more general criticism of program correctness, which seems valid to
me, is that proofs of program correctness are themselves much harder to be
sure of than the original programs.  The proofs of correctness of even very
simple programs can become extremely unwieldy.  This raises the question of
the worth of a proof that could be wrong, if the program itself is easier to
check by standard methods without a proof.  On the other hand, having a
proof may increase one's degree of confidence in the program's correctness,
despite the fact there's still a chance both the program and the proof could
be wrong.  One proposed solution is to not waste time verifying individual
programs, but to have *programs* that prove correctness--though of course
these programs need to be checked.  And, one program can check another,
though we know by Turing that there's an absolute limit to this.

    On the other hand, I don't want to claim computer science *is* a formal,
mathematical discipline.   I tend to think there was an interaction between
the engineering and the formal sides of computer science as it developed.
I think the mathematical discoveries in the 30's gave c.s. a tremendous
boost, but I think historically the engineering side came first.   If it's
to be argued whether c.s. is really engineering or whether it's really, say,
an implementation of recursive function theory, then I think the argument
would depend upon what is meant by "really".

Charlie Silver