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