Hacker News Reader

Comment by ChristianMarks | Hacker News Reader

The problems the OP wants to solve are formally undecidable and reducible to the halting problem.

1. Given a formal specification, find a program that meets the specification.

2. The apparently simpler problem of checking whether a given program meets a specification.

Both are undecidable. That said, there is an extensive literature on practical approaches to this problem. They generally suffer from intractability.

http://cfpm.org/pub/papers/tiofdm.pdf

I suggest looking at Robert Harper's book on type theory instead.

View on HN

I agree with the sentiment that the problem the OP brings up is difficult, but bringing up the halting problem here seems pretty pedantic.

If you restrict yourself to a turing incomplete language, checking a specification no longer reduces to the halting problem. In fact, there are many systems that do exactly this, and most of these systems are perfectly capable of sorting a list and proving that the list is sorted.

However, I think the real point is that there are at least dozens of smart people who are working on this exact problem all day, every day. The OP shows neither a deep understanding of why previous attempts at this have failed or really, any knowledge at all about the state of the field of programming language research.

Can you provide links to papers which try address this problem in practical terms, or some leads that one might use to acquaint themselves on the current state of research in this area? The paper the parent links I've only skimmed but what it seems to be advocating seems not to be that far from test-driven development. Has anyone tried anything more closely resembling what the OP is proposing? Are any such attempts doomed fromt he start?

You are right, I'm not intimately familiar with all the research out there and with all the details. I do think I have some useful things to add, that a "practical" angle is missing in many approaches, and that many attempts fail just because they get lost in trying to achieve theoretically elegant solutions, rather than building practical tools.

At least, I'll learn a lot. At most, we get something new with the help of other people.

The thing about the halting problem, though, is that it doesn't say "You can't write a program that can determine if another program will terminate". It says "You can't write a program that can determine if any other program will terminate."

Case in point: Resharper will tell me "This function never returns" in cases where it obviously wont return, and also offer to simplify methods that only ever return a single value despite what looks like a complex set of if-statements.

So, if it is possible to write a program to determine if a specific subset of all possible programs will terminate, is it possible to write a program that can generate a subset of all possible programs from a specific subset of all possible specifications?

I can't be perfect. But might it be useful?

This! That's why the halting problem is not an issue. Yes, it's impossible to solve in the general case. It doesn't mean it's definitely possible to solve it in 99% of your everyday programming work. Isn't that valuable? Isn't that worth an attempt at getting there?

The problems the OP wants to solve are formally undecidable and reducible to the halting problem.

While this is true in general, our current "solution" to the problem - hire a human programmer, give him the spec, and set him loose - doesn't do any better here. The problems we as an entire field "want to solve" are, in general, formally undecidable and reducible to the halting problem, but we get by anyways because it turns out that you can get a lot of useful work done even without solving the general problem.

I see no reason that a well-designed system couldn't similarly leverage "special cases" that are not undecidable. How efficiently this could be done is another matter, but I think step one in that direction is to accept a pretty major loss of generality - after all, that's how humans get the job done, and for the most part we're still able to turn most of the specs that we're faced with into working code, given enough time.

I have a question about this Christian, assume that we can accurately model an atom with a computer and then we uploaded a human into the computer, wouldn't the computer then be able to either solve the problem or report that the problem is unsolvable? I understand the halting problem but isn't there some kind of meta check that a sufficiently complex system could output?

Sure, having a virtual human try to solve the problem would be pretty good. However, even the virtual human would never be able to check the specification correctly for every possible program due to the halting problem. In particular, no matter what the specification was, a malicious user could create a program that mimics the virtual human's response and then does the opposite thing (it's the same basic proof that the halting problem is undecidable). By construction then, the virtual human would answer incorrectly when asked whether or not the program matches the specification.

So, academically, even the "virtual human" approach doesn't work since it doesn't answer correctly for every single program. Practically, you're right, having a virtual human would be good enough for most uses.

That said, I wouldn't want to use a virtual human for this due to ethical concerns :-).

The problem is that even real live humans can't always tell if something will halt. For instance, you tell me if this loop ends:

    n = 4;
    goldbach = true;
    while(goldbach) {
        goldbach = isSumOfTwoPrimes(n);
        n += 2;

You just have to prove the Goldbach Conjecture. :-)

Reply on news.ycombinator.com