4 ms·

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 o

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.

xyzzyz 7y ago
> 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?
- ahelwer 7y ago
  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
- YeGoblynQueenne 7y ago
  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)
hprotagonist 7y ago
>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.
pjc50 7y ago
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.
mcqueenjordan 7y ago
> 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.
- ahelwer 7y ago
  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.
- UncleMeat 7y ago
  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.

xyzzyz 7y ago

> 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?

ahelwer 7y ago
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
YeGoblynQueenne 7y ago
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)

hprotagonist 7y ago

>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.

pjc50 7y ago

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.

mcqueenjordan 7y ago

> 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.

ahelwer 7y ago
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.
UncleMeat 7y ago
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.