-------[beginning of reply of A. Bauer]-----------
From Andrej_Bauer@gs2.sp.cs.cmu.edu Fri Apr 16 14:57:55 1999
>
> BEGIN DORON ZEILBERGER's OPINION 37
>
> Opinion 37: Guess What? Programming is Even More Fun Than Proving, and, More
> Importantly It Gives As Much, If Not More, Insight and Understanding
>
First a comment:
There is a formal sense in which proving and programming are
equivalent. Under the Curry-Howard isomorphism, proposition are
interpreted as types, and types are interpreted as proposition.
Under the same isomorphism, proofs correspond to programs, and
vice versa. (For example, the program (lambda x:A. ), whose
type is A --> (A x A), proves the proposition A ==> (A and A).
Second, I have two questions:
#1: "All these algorithms that you have invented, someone had to PROVE
that they work, right?"
So, there is no fear that we're going to run out of things that
need to be proved.
#2: "All these programs that you have implemented, NOBODY has EVER
PROVED that they work, right?"
They are written in Maple, and Maple does not have a well-defined
semantics, hence, as far as mathematical standards of proof are
concerned, you have no idea whether they work.
I am well aware that your programs work in practice and have never
made a mistake. But that's beside the point.
What I am driving at is that Maple and Mathematica lack mathematical
rigor, because they are BADLY DESIGNED. There is no mathematical basis
on which they are built.
Maple and Mathematica are just as informal as the 18th century
mathematical analysis. It worked most of the time, but it didn't have
a proper foundation. With this picture in view you may understand why
mathematicians are largely unwilling to use your new tools.
I have worked extensively with Mathematica. It is easy to write a
100 line program in it. It is nearly impossible to write a 3000 line
theorem prover and guarantee that it works. In fact, I guarantee
that it doesn't work. The phrase "this Mathematica program is correct"
is not even well-defined!
Andrej Bauer
-----[end of reply of A. Bauer]-----
----reply from Richard Stanley-------
From rstan@math.mit.edu Sat Apr 17 20:07:38 1999
Dear Doron,
Just one comment on your opinion 37:
> Could you imagine Alain Connes writing a paper entitled `A new proof
> of 21x31=651'?
The only reason I can't imagine such a thing is that I can't imagine a
new proof that would be of interest to mathematicians. If Alain Connes
actually found an interesting new proof that gives new insight into
21x31=651 then I would be quite eager to read it, even though there
is a well-known and simple algorithmic proof.
Best regards,
Richard
---end reply from Richard Stanley-----