Comment by hollerith | Hacker News Reader

Comment by hollerith | Hacker News Reader

Parent Full thread

>To judge the impact of future use, you'd pretty much have to both 1) invent all the important uses, 2) judge the market impact of each

We are in disagreement here about how prediction works even after your use of the qualifiers "pretty much" and "important" is taken into account. (I should add that I am not saying that there is nothing to your assertion in grandparent, just that it is not the whole story and is too pessimistic about the human ability to predict.)

Parenthetically, I once got into a similar disagreement on Less Wrong -- with someone who claimed that the only way to predict any aspect of the outcome of a computer program was to run the program. So let me get your opinion on that, and let me use Dijkstra to choose a unambiguous question to ask you:

Dijkstra claimed that a person could arrive at a high confidence that a program has particular useful properties (e.g., that a program that keeps tracks of balances in bank accounts obeys the "law of the conservation of money") without ever running the program but rather by developing a proof of the "correctness" of a program (using techniques whose development form a large part of Dijkstra's reputation) at the same time one develops the program. Do you disagree with Dijkstra? I'm interested in replies from others too.

I agree with him in a limited scope :D

Certain class of programs is written with the explicit (or at least implicit) goal of having provable properties. Like (hopefully) the program the bank uses to track account balance.

However, a seemingly much easier problem (the Halting Problem [1]) is undecidable in the general case. One can find out at least some properties of some programs some of the time with certainty (modulo mundane mistakes). But one cannot find all the properties of all the programs all of the time.

Now perhaps programming isn't the best model of all human activities, but! If we were to narrow down the discussion to research on Computer Science alone -- it is proved (via the Halting Problem), that you can't know all the outcomes of every possible programs ahead of the time. Which means, research on some (possibly valuable) programs can't be graded with 100% certainty ahead of the time, because there is no way of knowing all the properties of a program in advance.

Back to the original topic, my point was -- if somebody invested effort into (honest, rigorous) research, it should not be derided, ever, as it may find unexpected, valuable uses. I don't claim anything about research pointed towards commercial (or otherwise) goals, except the general ``it's important, too -- but it's is not the only way we should follow''.

Back to the matter of predicting: I am convinced, in general, you can't predict some of the outcomes of research -- and some applications of the results. Moreover, I believe that among what can't be predicted, are many of the innovations and discoveries.

Now economic predictions (this will sell/this won't sell) are wrong some of the time. To prevent a wrong prediction from blocking research, there is usually pool of money for `blue-sky research', generally realized as countries sponsoring academiae, and individuals financing research out of own pocket.

It may be very hard to estimate effects of mis-predictions on research, due to this continuous financing -- financing that's independent of whether there is a clear, short-term goal for the research.

EDIT: the Rice's theorem, posted by sid0 [2], is a much better example.

EDIT2: as a funny corollary to the Halting Problem, in some cases even running the program won't give you a definite answer -- the program may go on endlessly. Running the program is not a fool-proof solution, thus not a general solution.

It follows your discussant was proven wrong (not completely right, to be exact) preemptively -- by Turing's proof of undecidability of the Halting Problem ;-)

----

[1] http://en.wikipedia.org/wiki/Halting_problem

[2] http://news.ycombinator.com/item?id=2392186

Thanks for the reply.

The person was talking about Rice's theorem [1], I believe. (It follows rather quickly from the unsolvability of the halting problem.) Proofs of program correctness might be exact for some programs, but Rice's theorem implies that you will never be able to come up with exact proofs for every program, and must rely on approximations. The entire field of program analysis and verification is dedicated to finding better approximations.

[1] https://secure.wikimedia.org/wikipedia/en/wiki/Rice%27s_theo...

Reply on news.ycombinator.com