4 ms·

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

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.

xyzzyz 7y ago
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.
- tathougies 7y ago
  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.
  - xyzzyz 7y ago
    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.
    - tathougies 7y ago
      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
- BeetleB 7y ago
  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.
  - xyzzyz 7y ago
    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.
  - YeGoblynQueenne 7y ago
    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.
copperx 7y ago
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.
gluelogic 7y ago
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

xyzzyz 7y ago

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.

tathougies 7y ago
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.
- xyzzyz 7y ago
  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.
  - tathougies 7y ago
    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
BeetleB 7y ago
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.
- xyzzyz 7y ago
  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.
- YeGoblynQueenne 7y ago
  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.

copperx 7y ago

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.

gluelogic 7y ago

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