Re: Transactions: good or bad?

Bob,

You claim that Alfredo didn't go over into philosophical grounds, I think it is the other way around. Indeed, in his first post he only claimed that computers do make proofs, and on the face of it, his claim is trivially true.

However the context of this discussion if you actually bother to read was the problem whether computers can create proofs of correctness, or incorrectness for that mater, for programs written by humans. This would require computers to solve problems no less general than an universal theorem solver. This is known (proven) to be impossible.

Even if we restrict the theorem solving capability to what humans can do, it is also well beyond the frontier of current science, and if we want to talk about beliefs of what science will do in the future we can go no further than to Hilbert, otherwise a brilliant mathematician, who held very strong *beliefs* about his program, beliefs which have been refuted only too soon after they were expressed.

It is obvious given the state of the science so far that computer proving is less general than human proving.

To quote J.Y. Girard: "Automatique proof ne fonctionne pas et ne fonctionnera jamais" (automatic proof doesn't work and it will never work). This is not a belief this a scientific statement coming from probably the most important logician of our times. It should be obvious both to you and to Alfredo that he knows about computerized proofs, but what he means is that computer will never be able to solve mathematical problems with the same generality as humans are capable of.

Furthermore, both you and Alfredo expressed the philosophical belief that human brain is in no way different than computers, Alfreado went even further into some "pauperistic" (Girard's word for popperism) beliefs with regards to proofs, scientific protocols and Mathematics not being a science (by Popper's beliefs of what science definition should be, it isn't, but who cares ?).

Both of you made trivial mistakes, like the ones with the game of chess, the last one you asked "Where's your proof that all chess games halt ?" . If I were to respond to that I'd have to consider you either incompetent or in trolling mode. The mission of a chess playing program is to decide the next best move and in so doing also evaluate a position, to which the problem whether there are infinite chess games is totally irrelevant. The same can be said of the situation where I claimed that mathematicians extend their models to which you reply that computers extends their theorem base, if you can't see the distinction, I frankly can't waste my time much longer.

If you want or not to subscribe to Alfredo's beliefs, I really don't care, but don't try to pass your beliefs for "science".

You should also take notice that "I disagree" with your characterization that I transformed this in a pissing match, and with regards to your :

"you might move the discussion in the direction of something truly illuminating. And who knows? You might inspire some anonymous lurker to pursue a path that leads to some truly important result."

I can only say that it has to get worse before it gets beter, there's no illuminating to be had in a piss poor exchange of trivialities, and I truly pitty the anonymous lurker who deludes himself that he can find truly important results departing from Usenet discussions.

A bon attendeur salut,
Costin Received on Mon Jun 16 2003 - 20:05:18 CEST