|
|
comp.lang.functional |
> He basically affirms without too much argumentation that automatic They are all the same problem in different incarnations. The days when people worried about mathematics because of #0 has long Theorem 0: Permanent employment of mathematicians. You will never run Theorem 2: Permanent employment of researchers in code optimization. So I don't see why we have to view #1 as a limitation rather than a Theorem 1: Permanent employment of researchers in automated reasoning. Costin Cozianu <c_cozi...@hotmail.com> writes: 1. Automated reasoning suffers from the Turing halting problem.
> I recently discovered the very opinionated and probably very well
> informed thoughts of one Jean Yves Girard who has some well deserved
> fame and notoriety in computer science and mathematics.
> proof doesn't work and will never work (basically because of the
> halting problem),
0. Mathematics suffers from the Goedel incompleteness and inconsistency
problem. (I know this is arguable, depending on what you consider
as the purpose of mathematics.)
2. Code optimization suffers from the Kolmogorov complexity problem.
gone. No one has ever used #2 to dismiss code optimization. In fact
both are now viewed optimistically and jokingly:
out of new axioms and new models to study.
You will always be able to publish new, better optimizations.
gift:
You can always find a way to beat your rival's automatic theorem
prover.