[I'd suggested that we take this discussion off the list. I'm continuing to reply here in this case only because I don't want people to get the incorrect idea that Godel's Incompleteness Theorem can be used to magically explain away any philosophical problem regarding computers.] OK, that one was mine. It wasn't in the context you originally quoted, or even from the same message you quoted (<19990405060635.29296.qmail(a)brouhaha.com>)m>). I had used it three hours earlier in the discussion (<19990405030452.28640.qmail(a)brouhaha.com>)m>). So perhaps you see why I didn't understand what you were complaining about. It is customary to include a brief quote of the actual context you are referring to. In the general case, I've never claimed that they do. I've only claimed that in a sufficiently limited problem domain with a time limit (i.e., the solution value vs. time curve is a flat with a sharp drop to zero), a computer may reach a better solution than a human would. I also claim that this is true for other common solution value vs. time curves; if the solution is worth $x today but only $x/2 tomorrow, the computer may produce a more valuable solution than would a human. [and later:] Sure. A human may proceed in a manner that is not based upon logical deduction or any (obvious) deterministic algorithm. It is yet to be proven that this human ability (as manifested in complex problem-solving) is not equivalent to a non-deterministic algorithm, or even to a sufficiently complex deterministic system. Penrose claims that quantum uncertaintly is necessary to intelligence. While he provides insufficient proof of this claim (really just anecdotal evidence), as an argument against machine intelligence it is a red herring, since it is not especially difficult to build a system that uses quantum uncertainty to influence nondeterministic algorithms. You know, since you mentioned the book GEB, I thought you might have been trying to bring Godel's Incompleteness Theorem into the discussion. But since you didn't specifically state that, I wanted to give you the benefit of the doubt. The Incompleteness Theorum if very useful for certain lines of reasoning. And it might be relevant to the strong AI problem. But it has no relevance to the compiler problem we've been discussing. In the compilers "axiomatic system", it is not possible to even construct the kind of questions to which GIT refers. The compiler is not burdened with proving that it is correct, or that its own output is correct. At most we are asking it to select the more efficient of several proposed solutions. This in some sense does involve a "proof", but the required proof is no of the validity of the axioms (i.e., the compiler algorithm), nor is it a proof that the "system" is self-consistent. If you know where to apply them. You can't just willy-nilly claim that GIT applies to any random problem. If you are going to maintain that GIT precludes compilers generating code as efficient as the best human-generated code, you'd best be prepared to present a logical argument as to why GIT applies. It's not a magic wand, and I'm not going to concede your point at the mere mention of it.