10 ms·

It's very cool how such a level of computational power is so seemingly easy to reach. I guess it's not surprising if you consider how simple Turing machines the

It's very cool how such a level of computational power is so seemingly easy to reach. I guess it's not surprising if you consider how simple Turing machines themselves are, but I'm always amazed that this is really enough.

vog 9y ago
The problem is exactly reverse: From a security and anaysis point of view, you want languages that do the job with the least possible power. And those are surprisingly hard to find. You start with simple and not too-powerful languages (rules systems, regexes, parsing stuff), note they are insufficient for some real-word use case, add one or two features, and bam!, that mess becomes turing complete.
- willtim 9y ago
  Strongly agree. With more constraints in the language, one gains greater power to reason. This is what the Ethereum creators are learning the hard way. I also think folks would be surprised with how much can be accomplished without Turing completeness. For example, merge sort can be implemented as a simple functional unfold, or "primitive corecursion" in a total language.
  - vog 9y ago
    > With more constraints in the language, one gains greater power to reason. Not only that, but you can also apply more tools onto it, treating the code as data and having a chance to use that as input data for totally different purposes. Another classic example is structured text. If you want to aggregate facts from that, this is totally easy when the data is available in a simple JSON structure. If it is a simple HTML site, this is slightly more involved: you need to scrape the site and recognize irrelevant stuff ( navigation bars, tables only used for layouting, etc.). But if it is a blob of Flash code that happens to display the text in some shiny way, you are essentially becoming a reverse engineer, and your tool will almost certainly break apart with every change / new version of that structured text.
  - cdancette 9y ago
    Because the number of operations in a sort is bounded. You can perform any sorting algorithm without turning completeness because you don't need the while loop basically.
    - pron 9y ago
      This applies to virtually any algorithm with a known bound. Any such algorithm can be carried out by primitive recursive functions. However, contrary to folklore, this makes absolutely no difference in verification complexity (see my other comment https://news.ycombinator.com/item?id=16383436 https://news.ycombinator.com/item?id=16383436). This can be easily shown by noting that we can assume -- with no loss of generality -- that any program is primitive recursive by implicitly adding a counter to each and every loop/recursive call, that counts down from, say, 2^500, and halts the program if it ever reaches zero (in fact, this is much more limited than primitive recursive as we're happy with a constant bound). As the counter will never reach zero in our physical universe, there is no change in program semantics, and therefore we can assume that all programs are written in non-Turing-complete languages if that were to help us in any way. Alas, as my other comment shows, it doesn't in the least.
  - pron 9y ago
    This is a very common misconception. While Turing complete computational models "suffer" from the halting problem that makes arbitrary "reasoning" uncomputable, that is 1. not quite the problem that makes reasoning hard, and 2. that does not mean that reasoning in weaker models is feasible. 1. What makes reasoning hard is not quite the halting theorem as normally stated, but a generalization of it that's sometimes called "bounded halting", and was used in the proof of the time-hierarchy theorem, possibly the most important theorem in theoretical computer science. Bounded halting roughly states that it's impossible to know in under N steps whether an arbitrary program P would halt when operating on input X in fewer than N steps. A simple corollary also shows the impossibility of generalizing the program's operation from one input to another. In short, this theorem means that it's impossible to know what a program would do for any input any faster than running it for every input. It can roughly be stated as saying that the verification or "reasoning" complexity for a program with a state space S of size |S| is θ(|S|) (where theta is like big-O, except it roughly means "no more and no less than", whereas big-O means "no more than"). Most importantly, this theorem does not require the programming model to be Turing complete. For example, it applies directly -- using the same proof -- to programming models that only allow primitive recursive functions. 2. Even the simplest computational model -- the barely useful finite-state machine -- is already too complicated for arbitrary reasoning. Its verification complexity also happens to be θ(|S|) (but with a different proof than that of the bounded halting theorem), where |S| is usually at least exponential in the size of the program. In general it can very easily be shown that if your programming languages has nothing more than boolean variables and the ability to write loops of length of no more than 2 or, alternatively, it has subroutines even if they cannot be recursive and there are no first-class subroutines -- reasoning is also infeasible (it's PSPACE-complete) and you might as well be Turing complete, as that won't make the worst-case any harder in practice (it makes no difference if the worst case is truly infinite or "just" much longer than the expected lifespan of the universe). The above fact means it is provably impossible to create a programming language -- no matter how limited -- where every program would be easily verifiable. To make a language feasibly verifiable in all/most cases, its state space must grow slowly (polynomially) with program size; this means that not only must the programming model be weak (basically just FSM), but the language exceptionally inexpressive. Regular expressions are pretty much the farthest we can go, and even then some simple questions about regexps are infeasible (such as whether two regexps are equivalent; I believe that problem is PSPACE complete, even though there are heuristic algorithms that work in many instances). For further discussion and complete results, see my post: https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity

vog 9y ago

The problem is exactly reverse: From a security and anaysis point of view, you want languages that do the job with the least possible power. And those are surprisingly hard to find. You start with simple and not too-powerful languages (rules systems, regexes, parsing stuff), note they are insufficient for some real-word use case, add one or two features, and bam!, that mess becomes turing complete.

willtim 9y ago
Strongly agree. With more constraints in the language, one gains greater power to reason. This is what the Ethereum creators are learning the hard way. I also think folks would be surprised with how much can be accomplished without Turing completeness. For example, merge sort can be implemented as a simple functional unfold, or "primitive corecursion" in a total language.
- vog 9y ago
  > With more constraints in the language, one gains greater power to reason. Not only that, but you can also apply more tools onto it, treating the code as data and having a chance to use that as input data for totally different purposes. Another classic example is structured text. If you want to aggregate facts from that, this is totally easy when the data is available in a simple JSON structure. If it is a simple HTML site, this is slightly more involved: you need to scrape the site and recognize irrelevant stuff ( navigation bars, tables only used for layouting, etc.). But if it is a blob of Flash code that happens to display the text in some shiny way, you are essentially becoming a reverse engineer, and your tool will almost certainly break apart with every change / new version of that structured text.
- cdancette 9y ago
  Because the number of operations in a sort is bounded. You can perform any sorting algorithm without turning completeness because you don't need the while loop basically.
  - pron 9y ago
    This applies to virtually any algorithm with a known bound. Any such algorithm can be carried out by primitive recursive functions. However, contrary to folklore, this makes absolutely no difference in verification complexity (see my other comment https://news.ycombinator.com/item?id=16383436 https://news.ycombinator.com/item?id=16383436). This can be easily shown by noting that we can assume -- with no loss of generality -- that any program is primitive recursive by implicitly adding a counter to each and every loop/recursive call, that counts down from, say, 2^500, and halts the program if it ever reaches zero (in fact, this is much more limited than primitive recursive as we're happy with a constant bound). As the counter will never reach zero in our physical universe, there is no change in program semantics, and therefore we can assume that all programs are written in non-Turing-complete languages if that were to help us in any way. Alas, as my other comment shows, it doesn't in the least.
- pron 9y ago
  This is a very common misconception. While Turing complete computational models "suffer" from the halting problem that makes arbitrary "reasoning" uncomputable, that is 1. not quite the problem that makes reasoning hard, and 2. that does not mean that reasoning in weaker models is feasible. 1. What makes reasoning hard is not quite the halting theorem as normally stated, but a generalization of it that's sometimes called "bounded halting", and was used in the proof of the time-hierarchy theorem, possibly the most important theorem in theoretical computer science. Bounded halting roughly states that it's impossible to know in under N steps whether an arbitrary program P would halt when operating on input X in fewer than N steps. A simple corollary also shows the impossibility of generalizing the program's operation from one input to another. In short, this theorem means that it's impossible to know what a program would do for any input any faster than running it for every input. It can roughly be stated as saying that the verification or "reasoning" complexity for a program with a state space S of size |S| is θ(|S|) (where theta is like big-O, except it roughly means "no more and no less than", whereas big-O means "no more than"). Most importantly, this theorem does not require the programming model to be Turing complete. For example, it applies directly -- using the same proof -- to programming models that only allow primitive recursive functions. 2. Even the simplest computational model -- the barely useful finite-state machine -- is already too complicated for arbitrary reasoning. Its verification complexity also happens to be θ(|S|) (but with a different proof than that of the bounded halting theorem), where |S| is usually at least exponential in the size of the program. In general it can very easily be shown that if your programming languages has nothing more than boolean variables and the ability to write loops of length of no more than 2 or, alternatively, it has subroutines even if they cannot be recursive and there are no first-class subroutines -- reasoning is also infeasible (it's PSPACE-complete) and you might as well be Turing complete, as that won't make the worst-case any harder in practice (it makes no difference if the worst case is truly infinite or "just" much longer than the expected lifespan of the universe). The above fact means it is provably impossible to create a programming language -- no matter how limited -- where every program would be easily verifiable. To make a language feasibly verifiable in all/most cases, its state space must grow slowly (polynomially) with program size; this means that not only must the programming model be weak (basically just FSM), but the language exceptionally inexpressive. Regular expressions are pretty much the farthest we can go, and even then some simple questions about regexps are infeasible (such as whether two regexps are equivalent; I believe that problem is PSPACE complete, even though there are heuristic algorithms that work in many instances). For further discussion and complete results, see my post: https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity