4 ms·

> The computing industry will get over its irrational fear of Turing. Undecidability is deeply misunderstood; undecideable problems must be solved, and are regu

by tromp 4y ago

> The computing industry will get over its irrational fear of Turing. Undecidability is deeply misunderstood; undecideable problems must be solved, and are regularly solved by any useful static analysis tool. Undecidable problems are not incomputable Here the author displays their own misunderstanding of undecidability. The fact that you can decide many instances of an undecidable problem doesn't change its undecidability in the least. Furthermore, when you consider computational hardness rather than undecidability, there are problems that are hard nearly everywhere (think of things like discrete log over elliptic curves), so there's no hope to approximate solutions.

Joker_vD 4y ago
Although, to be fair, undecidability often does serve as a blanket "do not even bother attempting this" refusal. But having a semi-algorithm with a work limiter bolted on ("if solution attempts take more than X operations and/or Y storage, declare failure") should often be pretty practical. After all, we already know of several theoretically exponential but practically linear problems.
Tainnor 4y ago
Yeah that part was basically where I stopped reading because it's clearly nonsense. Point 3 about the "outdated computing models from the 1940s and 50s" also ignores the fact that Turing machines are provably equivalent or stronger than any other system of computing ever conceived.
- TuringTest 4y ago
  It's no nonsense in the terms that it is explained: although a problem may be mathematically undecidable, it may still be a solved problem in practical terms - i.e. as finding good enough solutions for real world instances. As for point 3, I'd say you're making the same mistake; a model may be mathematically powerful yet practically unwieldy, and computing models from the 50's suffer this problem. Brainfuck is Turing-complete yet it would not make sense to recommend using it because it is provably equivalent or stronger than any other system of computing. Similarly, the Von-Neumann architecture was a great solution for computing physics problems with the electronics available in the 50's, but basing every modern programming language on that paradigm is a mistake.
  - Tainnor 4y ago
    > It's no nonsense in the terms that it is explained: although a problem may be mathematically undecidable, it may still be a solved problem in practical terms - i.e. as finding good enough solutions for real world instances. This is well known, that's the whole reason for formal methods in CS or of languages like Coq, Idris and so on. There is nothing revolutionary about it. The author should probably spend more time explaining why they think we will see a golden age of formal methods when the industry has consistently been pointing in a different direction for decades, instead of making vague associations or insinuating that we "misunderstand" Turing. > As for point 3, I'd say you're making the same mistake; a model may be mathematically powerful yet practically unwieldy, and computing models from the 50's suffer this problem. Compilers, interpreters etc. can easily translate between equivalent computational models (e.g. Lambda calculus and Turing machines), but the formal results, including undecidability, apply to all of them. So it doesn't matter that a Turing machine is hard to program; nobody wants to actually use it as a programming language. It's a computational model. > Similarly, the Von-Neumann architecture was a great solution for computing physics problems with the electronics available in the 50's, but basing every modern programming language on that paradigm is a mistake. I would say that, if you make such a claim, you should state why it is a mistake and what should be done instead.
    - TuringTest 4y ago
      > I would say that, if you make such a claim, you should state why it is a mistake and what should be done instead. Others have explained the problem with the von Neumann bottleneck,[1][2] and ways to overcome it or even redefine it.[3] The industry is evolving towards programming paradigms less affected by that original computation model such as functional, functional-reactive, or agent-based programming(*), yet most of those are still converted down to Von-Neumann-style runtimes to be processed. Now that machine learning is increasingly being used to solve new problems, many computations may be done with dedicated non-VN hardware like tensor processors or analog computers (which are coming back with a vengeance). (*) Listed in increasing order of real-world expressivity, although their computational expressivity in all them is mathematically equivalent to Brainfuck. [1] https://dl.acm.org/doi/10.1145/1283920.1283933 https://dl.acm.org/doi/10.1145/1283920.1283933 [2] https://www.techtarget.com/whatis/definition/von-Neumann-bottleneck https://www.techtarget.com/whatis/definition/von-Neumann-bot... [3] https://www.sigarch.org/the-von-neumann-bottleneck-revisited/\ https://www.sigarch.org/the-von-neumann-bottleneck-revisited...*
jcranmer 4y ago
Any algorithm can be made to create "yes", "no", and "I don't know" buckets, and all undecidability means is that "I don't know" cannot be empty. I don't really know of any case where undecidability truly caused people to shy away from attempting to solve problems: static analysis is frequently undecidable and yet it's a fairly thriving field.
- Tainnor 4y ago
  As a hard result, undecidability may be unimportant. Someone rarely wants to know whether a Gödel sentence is "true" or determine whether a program that references itself halts. But such theorems, by placing a theoretical, if contrived, limit, often seem to have a qualitative implication as well: namely that solving the problem in the general case, even if we manage to exclude pathological cases, is hard or even unfeasible. It seems consistent with the fact that there is no known algorithm for deciding whether a theorem is true, or for accurately and fully predicting the behaviour of arbitrary programs. As you said, that doesn't make formal methods useless. But it reframes the discussion away from trying to find a universal problem solver towards discussing tradeoffs (e.g. pushing the proof burden to the programmer, rejecting valid programs, or using imperfect heuristics).

by tromp 4y ago

Joker_vD 4y ago

Although, to be fair, undecidability often does serve as a blanket "do not even bother attempting this" refusal. But having a semi-algorithm with a work limiter bolted on ("if solution attempts take more than X operations and/or Y storage, declare failure") should often be pretty practical. After all, we already know of several theoretically exponential but practically linear problems.

Tainnor 4y ago

Yeah that part was basically where I stopped reading because it's clearly nonsense. Point 3 about the "outdated computing models from the 1940s and 50s" also ignores the fact that Turing machines are provably equivalent or stronger than any other system of computing ever conceived.

TuringTest 4y ago
It's no nonsense in the terms that it is explained: although a problem may be mathematically undecidable, it may still be a solved problem in practical terms - i.e. as finding good enough solutions for real world instances. As for point 3, I'd say you're making the same mistake; a model may be mathematically powerful yet practically unwieldy, and computing models from the 50's suffer this problem. Brainfuck is Turing-complete yet it would not make sense to recommend using it because it is provably equivalent or stronger than any other system of computing. Similarly, the Von-Neumann architecture was a great solution for computing physics problems with the electronics available in the 50's, but basing every modern programming language on that paradigm is a mistake.
- Tainnor 4y ago
  > It's no nonsense in the terms that it is explained: although a problem may be mathematically undecidable, it may still be a solved problem in practical terms - i.e. as finding good enough solutions for real world instances. This is well known, that's the whole reason for formal methods in CS or of languages like Coq, Idris and so on. There is nothing revolutionary about it. The author should probably spend more time explaining why they think we will see a golden age of formal methods when the industry has consistently been pointing in a different direction for decades, instead of making vague associations or insinuating that we "misunderstand" Turing. > As for point 3, I'd say you're making the same mistake; a model may be mathematically powerful yet practically unwieldy, and computing models from the 50's suffer this problem. Compilers, interpreters etc. can easily translate between equivalent computational models (e.g. Lambda calculus and Turing machines), but the formal results, including undecidability, apply to all of them. So it doesn't matter that a Turing machine is hard to program; nobody wants to actually use it as a programming language. It's a computational model. > Similarly, the Von-Neumann architecture was a great solution for computing physics problems with the electronics available in the 50's, but basing every modern programming language on that paradigm is a mistake. I would say that, if you make such a claim, you should state why it is a mistake and what should be done instead.
  - TuringTest 4y ago
    > I would say that, if you make such a claim, you should state why it is a mistake and what should be done instead. Others have explained the problem with the von Neumann bottleneck,[1][2] and ways to overcome it or even redefine it.[3] The industry is evolving towards programming paradigms less affected by that original computation model such as functional, functional-reactive, or agent-based programming(*), yet most of those are still converted down to Von-Neumann-style runtimes to be processed. Now that machine learning is increasingly being used to solve new problems, many computations may be done with dedicated non-VN hardware like tensor processors or analog computers (which are coming back with a vengeance). (*) Listed in increasing order of real-world expressivity, although their computational expressivity in all them is mathematically equivalent to Brainfuck. [1] https://dl.acm.org/doi/10.1145/1283920.1283933 https://dl.acm.org/doi/10.1145/1283920.1283933 [2] https://www.techtarget.com/whatis/definition/von-Neumann-bottleneck https://www.techtarget.com/whatis/definition/von-Neumann-bot... [3] https://www.sigarch.org/the-von-neumann-bottleneck-revisited/\ https://www.sigarch.org/the-von-neumann-bottleneck-revisited...*

jcranmer 4y ago

Any algorithm can be made to create "yes", "no", and "I don't know" buckets, and all undecidability means is that "I don't know" cannot be empty. I don't really know of any case where undecidability truly caused people to shy away from attempting to solve problems: static analysis is frequently undecidable and yet it's a fairly thriving field.

Tainnor 4y ago
As a hard result, undecidability may be unimportant. Someone rarely wants to know whether a Gödel sentence is "true" or determine whether a program that references itself halts. But such theorems, by placing a theoretical, if contrived, limit, often seem to have a qualitative implication as well: namely that solving the problem in the general case, even if we manage to exclude pathological cases, is hard or even unfeasible. It seems consistent with the fact that there is no known algorithm for deciding whether a theorem is true, or for accurately and fully predicting the behaviour of arbitrary programs. As you said, that doesn't make formal methods useless. But it reframes the discussion away from trying to find a universal problem solver towards discussing tradeoffs (e.g. pushing the proof burden to the programmer, rejecting valid programs, or using imperfect heuristics).