15 ms·

> have only found constructed examples, mostly minor variations on the same "diagonalization" argument Anything that is Turing-complete cannot be implemented i

> have only found constructed examples, mostly minor variations on the same "diagonalization" argument Anything that is Turing-complete cannot be implemented in Ld (by definition). Off the top of my head, this includes: Recurrent Neural Networks, CSS, Minecraft, TrueType fonts, x86 emulators (MOV is Turing-complete) and Conways' Game of Life. Of course you can argue that lots of things can be implemented in an Ld language. Sure, I have nothing against it, but it's not like desiring Turing-completeness is an absurd requirement. > Any algorithm that is known to work is necessarily in Ld No, most algorithms are known to work correctly for the common cases that are tested for + all the edges cases the developers can think of or encounter in real life. For non-trivial software, this is a minuscule subset of the possible states. Lots of things are surprisingly Turing-complete, and it is not trivial to prevent this for a sufficiently complex system.

lmm 9y ago
> Anything that is Turing-complete cannot be implemented in Ld (by definition). Off the top of my head, this includes: Recurrent Neural Networks, CSS, Minecraft, TrueType fonts, x86 emulators (MOV is Turing-complete) and Conways' Game of Life. You're begging the question - your Turing-complete algorithm is "evaluate an expression in a Turing-complete language". It's easy to make a language accidentally Turing-complete (especially when you're thinking in a Turing-complete language), but that completeness is undesirable, and in realistic use cases it's harmful rather than helpful. No-one wants to sit waiting indefinitely to see whether a web page or font is actually going to render or not (and indeed we often end up going to great lengths to make these things Turing-incomplete in practice with timeouts and the like). > No, most algorithms are known to work correctly for the common cases that are tested for + all the edges cases the developers can think of or encounter in real life. For non-trivial software, this is a minuscule subset of the possible states. You're not contradicting me, you're saying "most algorithms are not known to work". I don't think that's true in the sense of "algorithms" published in journals/textbooks. I would agree that most code isn't known to work, but that translates into reality: most code doesn't work, most programs have cases where they just break and also just crash every so often. > Lots of things are surprisingly Turing-complete, and it is not trivial to prevent this for a sufficiently complex system. For a complex system written from scratch, it's easy enough with the right tools. If you build it in a non-Turing-complete language it won't be Turing-complete, and if something is hard to do in a total way it's probably a bad idea. Porting an existing system would be much harder, I'll agree, and porting the existing code/protocol ecosystem would be a huge ask. (I do think it's necessary though; the impact of malware attacks gets worse every day, the level of bugginess we're used to seeing in software is rapidly ceasing to be good enough).
- pron 9y ago
  This entire discussion about Turing completeness is completely irrelevant. The problem that's relevant to software verification isn't the halting problem in its original formulation, but a simple corollary of it, often called "bounded halting" (which serves as the core of the time hierarchy theorem, possibly the most important theorem in computer science), which states that you cannot know whether a program halts within n steps in under n steps. The implication is that there can exist no general algorithm for checking a universal property (e.g. the program never crashes on any input) that is more efficient than running the program on every possible input until termination. But bounded halting holds not only for Turing complete languages, but for total languages, too (using the same proof). In fact, it holds even for finite state machines (with a different proof). This is why even the verification of finite state machines is generally infeasible (or very expensive under restricted conditions) both in theory and in practice.
  - lmm 9y ago
    To my mind all that says is that even general total languages or finite state machines allow expressing too much. Surely one can solve this by working in a language where functions are not merely total but come with explicit bounds on their runtime. This seems like a good fit for a stratified language design like Noether - we might have to resort to including a few not-provably-bounded total functions (or even not-provably-total functions) in a practical program, but hopefully would be able to minimize this and make the parts where we were making unproven assumptions very explicit.
    - pron 9y ago
      There are languages where all functions run in PTIME (https://www.cs.toronto.edu/~sacook/homepage/ptime.pdf https://www.cs.toronto.edu/~sacook/homepage/ptime.pdf), but this doesn't help. If your program is a FSM, then your functions run in constant time, and still verification is infeasible. Search for "Just as a quick example of why verifying even FSMs is hard" in my blog post http://blog.paralleluniverse.co/2016/07/23/correctness-and-complexity/ http://blog.paralleluniverse.co/2016/07/23/correctness-and-c... Languages that are so limited as to be unusable are still PSPACE-complete to verify. It is simply impossible to create a useful programming language where every program is easily verifiable. Propositional logic -- the simplest possible (and too constrained to be useful) "language" -- is already intractable. Feasible verification in the worst-case and computation of even the most limited kind are simply incompatible. As anyone who has done any sort of formal verification -- it's hard. There are two general ways of getting around this difficulty. Either we verify only crude/local properties using type checking/static analysis (both are basically the same abstract interpretation algorithm), or taylor a verification technique to a small subset of programs. The other option is, of course, to work hard.

lmm 9y ago

> Anything that is Turing-complete cannot be implemented in Ld (by definition). Off the top of my head, this includes: Recurrent Neural Networks, CSS, Minecraft, TrueType fonts, x86 emulators (MOV is Turing-complete) and Conways' Game of Life. You're begging the question - your Turing-complete algorithm is "evaluate an expression in a Turing-complete language". It's easy to make a language accidentally Turing-complete (especially when you're thinking in a Turing-complete language), but that completeness is undesirable, and in realistic use cases it's harmful rather than helpful. No-one wants to sit waiting indefinitely to see whether a web page or font is actually going to render or not (and indeed we often end up going to great lengths to make these things Turing-incomplete in practice with timeouts and the like). > No, most algorithms are known to work correctly for the common cases that are tested for + all the edges cases the developers can think of or encounter in real life. For non-trivial software, this is a minuscule subset of the possible states. You're not contradicting me, you're saying "most algorithms are not known to work". I don't think that's true in the sense of "algorithms" published in journals/textbooks. I would agree that most code isn't known to work, but that translates into reality: most code doesn't work, most programs have cases where they just break and also just crash every so often. > Lots of things are surprisingly Turing-complete, and it is not trivial to prevent this for a sufficiently complex system. For a complex system written from scratch, it's easy enough with the right tools. If you build it in a non-Turing-complete language it won't be Turing-complete, and if something is hard to do in a total way it's probably a bad idea. Porting an existing system would be much harder, I'll agree, and porting the existing code/protocol ecosystem would be a huge ask. (I do think it's necessary though; the impact of malware attacks gets worse every day, the level of bugginess we're used to seeing in software is rapidly ceasing to be good enough).

pron 9y ago
This entire discussion about Turing completeness is completely irrelevant. The problem that's relevant to software verification isn't the halting problem in its original formulation, but a simple corollary of it, often called "bounded halting" (which serves as the core of the time hierarchy theorem, possibly the most important theorem in computer science), which states that you cannot know whether a program halts within n steps in under n steps. The implication is that there can exist no general algorithm for checking a universal property (e.g. the program never crashes on any input) that is more efficient than running the program on every possible input until termination. But bounded halting holds not only for Turing complete languages, but for total languages, too (using the same proof). In fact, it holds even for finite state machines (with a different proof). This is why even the verification of finite state machines is generally infeasible (or very expensive under restricted conditions) both in theory and in practice.
- lmm 9y ago
  To my mind all that says is that even general total languages or finite state machines allow expressing too much. Surely one can solve this by working in a language where functions are not merely total but come with explicit bounds on their runtime. This seems like a good fit for a stratified language design like Noether - we might have to resort to including a few not-provably-bounded total functions (or even not-provably-total functions) in a practical program, but hopefully would be able to minimize this and make the parts where we were making unproven assumptions very explicit.
  - pron 9y ago
    There are languages where all functions run in PTIME (https://www.cs.toronto.edu/~sacook/homepage/ptime.pdf https://www.cs.toronto.edu/~sacook/homepage/ptime.pdf), but this doesn't help. If your program is a FSM, then your functions run in constant time, and still verification is infeasible. Search for "Just as a quick example of why verifying even FSMs is hard" in my blog post http://blog.paralleluniverse.co/2016/07/23/correctness-and-complexity/ http://blog.paralleluniverse.co/2016/07/23/correctness-and-c... Languages that are so limited as to be unusable are still PSPACE-complete to verify. It is simply impossible to create a useful programming language where every program is easily verifiable. Propositional logic -- the simplest possible (and too constrained to be useful) "language" -- is already intractable. Feasible verification in the worst-case and computation of even the most limited kind are simply incompatible. As anyone who has done any sort of formal verification -- it's hard. There are two general ways of getting around this difficulty. Either we verify only crude/local properties using type checking/static analysis (both are basically the same abstract interpretation algorithm), or taylor a verification technique to a small subset of programs. The other option is, of course, to work hard.