Hacker News Reader

Comment by ahelwer | Hacker News Reader

There's a flipside of this, where people incorrectly lord "mathematical impossibility" over others as a way to shut down discussion. You see this on the topic of cryptographic backdoors especially. I'm against cryptographic backdoors, but claiming they're not technically possible is a losing position.

The interface between plain language and math is messy. I don't think I've ever seen something suggested that was actually mathematically impossible. Even the halting problem is easily solved in practice.

View on HN

This is where a very carefully worded description of the problem may be required.

Cryptographic backdoors are possible (See Clipper and LEAF for previous examples). Cryptographic backdoors that will only ever be used "legitimately" aren't, and legitimacy isn't a mathematical concept.

>Even the halting problem is easily solved in practice.

no, it's not. Knowing that this specific program halts or not doesn't address the issue.

> Even the halting problem is easily solved in practice.

You don't grok what the halting problem is. What you're describing (I assume) is determining if a specific program is going to terminate. That's not the same problem.

From Wikipedia:

Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist.

The entire field of static analysis is "solving" undecidable problems effectively and productively all the time. Just accept a few false positives or false negatives and suddenly the field opens up to be amazingly useful.

Yes it isn't literally solving the halting problem. But I've had a weird number of people tell me that the stuff I work on doesn't work because of things they learned in undergrad.

I "grok" very well what the halting problem is, thank you. It's colloquially used in the sense of being unable to tell whether a program terminates. For reference I direct you to early static analysis tool promo materials (ex. Coverity) which usually explicitly address the "doesn't this run into the halting problem?" question given its common occurrence.

> I'm against cryptographic backdoors, but claiming they're not technically possible is a losing position.

I never seen anyone serious ever claim that cryptographic backdoors are impossible.

> Even the halting problem is easily solved in practice.

Like, how exactly?

If you're writing business logic in a modern programming language your code can almost certainly be proven to halt. Very few people are running around coding up the Collatz conjecture or feeding programs as input to themselves.

It's clearly not true in any practical way. because most programs these days are huge beasts depending on stacks of millions of lines of code, so little can be conclusively proven about those. It's also wrong in theoretical sense, because what you're talking about is not "halting problem" at all.

Can't speak for ahelwer, but once at work we had to show (for certification purposes), that our program wouldn't get lost in an infinite loop.

Now from a realistic standpoint, all they wanted was some evidence we had considered this possibility and some data/argument to show our confidence that it wouldn't.

This was a simple program - you could confirm the algorithm wouldn't run forever by examining the code - look at the loops and their termination conditions, and look at function calls to show there were no loops in the call graph, etc. Yet one engineer in the team refused to engage. He kept invoking the halting problem. At one point I asked him that if the program was simply 'print "A"' would he still refuse to make the claim? Yup. No idea what the compiler/interpreter/HW is doing behind the scenes.

In the real world, when someone asks you to give an idea as to whether the program could hang in an infinite loop, don't invoke the Halting Problem. You're not answering the question they think they are asking, and as an engineer, your job is not to be pedantic with customers - unless you want to lose them fast.

Yes, people who are clueless about what halting problem is, shouldn't invoke it. Halting problem is not about impossibility to prove that any specific program fails, it's about impossibility to create a program that would take any program as its input and automatically answer whether that one halts or not.

In a company I worked for, systems were brought to their knees because of a while loop that went infinite under poorly tested conditions. There was a meeting and the head of the dev team came down to tell us that, in the meeting, it was decided that we should not use iteration any more because it runs the risk of going infinite. Instead, we should use recursion for all our looping needs.

That was in a C# shop so of course the "decision" was never implemented. My guess is that this was a completely mad decision taken by non-technical managers in a moment of panic, who had pressed our tech lead a bit too much on why software breaks and what can be done to avoid it breaking- and then latched on to some off-hand comment about recursion being an alternative to iteration, and ran with it.

Their head probably would have exploded when they saw what the C# compiler did with tail recursive functions . :-D

I think this really depends on how much you're willing to assume. You are right of course that the general problem is intractable, because you'd end up having to analyze frameworks, system calls, kernels, etc. But if you are able to assume those function as stated, then yes, you can certainly prove limited facts. For example, the sel4 microkernel is proven correct. Part of this proof of correctness is that all system calls do terminate.

But, actually, the most straightforward way to show that most 'everyday' programs terminate is -- assuming functionality of the language runtime as stated -- that they typically consist of non-recursive functions or functions on structurally smaller inputs. It would be obnoxious, but not difficult to show that a program like 'grep' terminates, assuming functionality of the operating system and hardware on which its running. This is actually fairly straightforwards, and many many functional languages with a focus on correctness have totality checking builtin. For example, Idris and Agda.

Of course, if you're going to ask to prove both functionality of the operating system (like Linux + glibc) or the processor itself, then that could indeed be trickier. But, if you limit your stack, it's certainly possible. The truth is that most computing does not consist of solving Turing complete problems.

Sure, with some copious assumptions about the environment, you can prove without great difficulty that many real world programs do terminate. But it has really nothing to do with the Halting Problem, and saying that "halting problem is easily solved in practice" is extremely misleading.

I mean in practice the halting problem is not a useful result either so... The halting problem is theoretically solvable on every computer known to mankind becayse every computer thus far is a finite state machine, not a turing machine. The halting problem on finite state machines is solvable (exhaustively check there are no loops -- the structural recursion check I suggested above is simply an optimization of this more general technique).

Now if we are actually discussing in good faith, the halting problem is often used as a reason why a particular program analysis wont work. While a good guideline, it does not mean that there are particular classes of programs for which these analyses would work. If you can show this and show that these programs cover a good amount of useful programs, then you can construct analyses that a purely theoretical and cursory understanding of the halting problem would suggest you cant. Indeed several useful languages do just this

This comment is not germane to the point you were making, just wanted to share:

I am a web dev who knows nothing of the Collatz conjecture, so I had to check out the Wikipedia article for it. Thanks for teaching me something today.

I wrote this JavaScript function based on what I read in the article. It's a simple algorithm but it was fun to see it work. For anyone who is in my shoes (weak mathematical background), running this function might be a useful supplement for illustrating the gist concept of the Collatz conjecture:

    function collatz(i) {
      console.log(i); // for visual feedback
      if (i <= 0) throw new Error('Input must be a positive integer');
      if (i === 1) return i;
      if (i % 2 === 0) return collatz(i/2);
      return collatz((3*i)+1);
    }

    collatz(42); // or any positive integer

Sure, you can do that with formal methods, but proving that a program is correct or that it halts is not the same as solving the halting problem.

That's not what the OP means, from what I can tell, but in the real world even a program like "while true {}" can be guaranteed to halt because eventually someone will figure out it's stuck in an infinite loop and abort it.

(tongue in cheek, of course, but I think the OP is trying to capture a similar pragmatic view of the halting problem)

Reply on news.ycombinator.com