7 ms·

> It is possible to write provably correct code. How many modern programmers hold this mistaken belief? It's false -- the Turing Halting problem (https://en.wi

by lutusp 11y ago

> It is possible to write provably correct code. How many modern programmers hold this mistaken belief? It's false -- the Turing Halting problem (https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem) demonstrates that one cannot establish that a non-trivial program is "provably correct." It seems the OP got carried away with his rhetoric, and the way he put it is simply wrong.

geofft 11y ago
That is a very common but incorrect misinterpretation of the halting problem. The halting problem says that there exist programs that cannot be proven correct; it says that for any property you want to prove computationally, no program can give you an answer for every last program. It doesn't say anything about "non-trivial" programs. In particular, if you write programs with awareness of the halting problem in mind, you can write extremely complicated programs that are provably correct. One straightforward way to do this is with a language that always halts. The proof assistant Coq is based on such a language, and it's powerful enough to write a C compiler: http://compcert.inria.fr/ http://compcert.inria.fr/ It is certainly correct that you can't stuff an arbitrarily vexatious program through a proof assistant and get anything useful on the other side. But nobody is interested in proving things about arbitrarily vexatious programs; they're interested in proving things about programs that cooperate with the proof process. If your program doesn't want to cooperate, you don't need an exact answer; you might as well just say "No, I don't care, I'm not trusting you."
- pekk 11y ago
  That is an incorrect misinterpretation of the posts you are responding to. If a programming language is Turing complete, then there is no way to prove that programs in that language halt in the general case (undecidable). The general case is important. It is not reasonable for a compiler which claims to detect halting to just bug out and refuse to compile certain valid programs. At best, people might still run a linting program which detects halting sometimes, but that flakiness is no good for the compiler. One of the implications of the halting problem is that a language in which all valid programs halt is not Turing complete. If you mean to say that you think programming's future is languages that are not Turing complete, just say so and then you can avoid delivering these condescending lectures to people who are operating under the reasonable assumption that future programming languages of general usefulness will be Turing-complete just like almost all the successful languages of the past have been.
  - geofft 11y ago
    No, I don't believe that the future is languages that are not Turing-complete, mostly because halting is not the property most people care about. I believe that a large part of the future will be languages that are not Turing-complete, for applications where that's appropriate (e.g., C compilers) but not where it's not (e.g., interpreters). I also don't think that "well, that's how we've always done it" is a particularly compelling argument given how young the field of programming languages is. For instance, another wonderful example of requiring code to cooperate with the proof process is Google's Native Client. NaCl doesn't care about halting; what it cares about is that the code in question only accesses its own memory, or makes specific pre-defined calls into the supervising code. You can do this with hardware support (and they did, with segmentation, where available), but you can also do this with software support. The NaCl technique is straightforward. You're required to lay out your assembly so that every 32-byte alignment boundary separates instructions; you must insert NOPs as necessary. Any fixed read, write, or jump must be within an address within a mask (or to a predefined address in privileged code), and any computed read, write, or jump must be immediately preceded, within the same 32-byte block, by a mask operation on the relevant register. For data, the mask enforces that only data is accessed; for jumps, the mask enforces that the jump target is within the code area and also 32-byte aligned. Now you've proven a fairly complicated property of the code, that control flow never escapes to privileged code except at well-defined entry points. Doing so on arbitrary x86 would be impossible (unless you resort to binary translation), but this is a very minor modification to arbitrary x86, and a regular C compiler can be easily modified to emit it. The resulting restricted variant of x86 remains Turing-complete. And it is entirely reasonable for the NaCl verifier to say "Uh, what are you doing, please try again" if presented with code that is technically non-malicious but does not follow the rules. The NaCl verifier doesn't claim to detect malicious code (that's the antivirus problem, and unsolvable). It claims to take code that makes a specific promise about not being malicious, and verifies that property.
    - dllthomas 11y ago
      "halting is not the property most people care about" I agree that non-Turing complete languages are hugely interesting and likely to be more important as we go forward. But not for this reason. Most of the non-trivial properties people do care about can be used to tell you if a program is going to halt in a finite amount of time. Want an upper bound on memory? This program doesn't have one? Well, then it never halts. It has one? Well, then we know it halts or loops within 2^bits steps - run it for that many steps and you know which. I think non-Turing-complete will prove interesting because our programs are currently described in Turing complete languages, but run in more constrained contexts anyway. A program that always halts after running for 2^100 steps is not Turing complete. A program that halts if it tries to use more than 2^100 bytes of memory is not Turing complete. Applying these constraints in this way doesn't help us with analysis much, but it hints that we can probably find other ways to constrain our programs which won't get in the way of what we're trying to accomplish, and it's quite possible that some of those will let us build languages more amenable to analysis (and further possible that the gains in analysis will make up for a limited amount of getting-in-the-way).
- Animats 11y ago
  Right. This is a bogus complaint about proof of correctness. The way you prove halting is to find some integer measure for each loop (like "iterations remaining" or "error being reduced") which decreases on each iteration but does not go negative. If you can't find such a measure, your program is probably broken. (See page 12 of [1], the MEASURE statement, for a system I built 30 years ago which did this.) The measure has to be an integer, not a real number, to avoid Zeno's paradox type problems. (1, 1/2, 1/4, 1/8, 1/16 ...) On some floating point problems, with algorithms that are supposed to converge, proving termination can be tough. You can always add an iteration counter and limit the number of iterations. Now you can show termination. Microsoft's Static Driver Verifier is able to prove correctness, in the sense of "not doing anything that will crash the kernel", about 96% of the time. About 4% of the time, it gives up after running for a while. If your kernel driver is anywhere near close to undecidability, there's something seriously wrong with it. In practice, this is not one of the more difficult areas in program verification. [1] http://www.animats.com/papers/verifier/verifiermanual.pdf http://www.animats.com/papers/verifier/verifiermanual.pdf
  - nickpsecurity 11y ago
    Pascal-F is interesting and not in my collection. What were most useful or interesting things you did with it? And does it have any use today in modern Pascal-like languages (maybe Modula-2 revision)?
- lutusp 11y ago
  > It doesn't say anything about "non-trivial" programs. No, but its source does. The source for the Turing Halting problem is Gödel's incompleteness theorems, which do specify that the entities to which it applies are non-trivial. The Turing Halting problem, and Gödel's incompleteness theorems, are deeply connected. > One straightforward way to do this is with a language that always halts. That doesn't avoid the halting problem, it only changes the reason for a halt. And it cannot guarantee that that program will (or won't) halt, if you follow -- only its interpreter. > In particular, if you write programs with awareness of the halting problem in mind, you can write extremely complicated programs that are provably correct. You need to review the Turing Halting problem. No non-trivial computer program can be proven correct -- that's the meaning of the problem. It cannot be waved away, any more than Gödel's incompleteness theorems can be waved away, and for the same reason.
  - deleted 11y ago
    [deleted]
  - geofft 11y ago
    > The source for the Turing Halting problem is Gödel's incompleteness theorems, which do specify that the entities to which it applies are non-trivial. The Turing Halting problem, and Gödel's incompleteness theorems, are deeply connected. Gödel doesn't say anything about "non-trivial" any more than Turing does. His first theorem is a "there exists at least one statement" thing, just like the halting problem. Like the halting problem, the proof is a proof by construction, but that statement is not a statement that anyone would a priori are to prove, just like the program "If I halt, run forever" is not a program that anyone would particularly want to run. So while yes, they're deeply connected, from the point of view of proving actual systems correct, it's not clear they matter. And neither theorem says anything about "non-trivial" statements/programs (just about non-trivial formalizations and languages). Gödel's second theorem is super relevant, though: it says that any consistent system cannot prove its own consistency. But that's fine. Coq itself is implemented in a Turing-complete language (ML), not in Coq. It would be nice if we could verify Coq in Coq itself, but since Gödel said we can't, we move on with life, and we just verify other things besides proof assistants. (And it seems to be worthwhile to prove things correct in a proof assistant, even without a computer-checked proof of that proof assistant's own correctness.) This is not waving away the problem, it's acknowledging it and working within the limits of the problem to do as much as possible. And while that's not everything, it turns out a lot of stuff of practical importance -- perhaps everything of practical importance besides proving the system complete in its own language -- is possible.
catnaroek 11y ago
Wrong. What Russell/Gödel/Turing/Rice/etc. tell you you can't do is write a decision procedure that checks arbitrary nontrivial properties of programs. In other words, if you first write a program and only then ask whether it is correct, you've already lost. Obviously, the solution is to stop writing arbitrary programs. As Dijkstra said long ago, we need to find a class of intellectually manageable programs - programs that lend themselves to being analyzed and understood. Intuitively, this is exactly what programmers demand when they ask for “simplicity”. The problem is that most programmers' view of “simplicity” is distorted by their preference for operational reasoning, eschewing more effective and efficient methods for reasoning about programs at scale.
- jonahx 11y ago
  Nice post. Can you clarify your last sentence? What do you mean by "preference for operational reasoning"? What's an example of the more effective methods for reasoning about programs at scale that you're contrasting this to?
  - catnaroek 11y ago
    “Operational reasoning” means using execution traces (the sequence of states underwent by a process under the control of your program) to derive conclusions about the program. You can do it in your head, using a piece of paper, using a debugger, using strategic assertions, etc. By “more effective methods for reasoning about programs at scale”, what I mean is analyzing the program in its own right, without reference to specific execution traces. There are several kinds of program analyses that can be performed without running the program, but, to the best of my knowledge, all of them are ultimately some form of applied logic.
  - klibertp 11y ago
    It's a guess, but I think GP uses "operational" as a synonym for "imperative". I think I encountered the term "operational semantics" in the context of Prolog programming. Denotational semantics is a term for a kind of semantics which are mathematically pure. IIRC Prolog has both operational and denotational semantics defined and they conflict. There's something about cut operator and tree pruning, but I read this long ago :-)
jahewson 11y ago
The Halting problem can already be solved for a non-trivial subset of programs, take a look at Microsoft Research's "Terminator" project: http://research.microsoft.com/apps/mobile/news.aspx?post=/en-us/news/features/terminator.aspx http://research.microsoft.com/apps/mobile/news.aspx?post=/en...
- kazinator 11y ago
  But the halting problem for a subset of programs isn't The Halting Problem, which is the question whether a UTM can exist to calculate any function, over its entire domain.
  - dllthomas 11y ago
    The parent's wording was a little sloppy, but the point was that the grandparent was incorrectly using the Halting Problem to argue that you can't even do it for a meaningful subset of programs, which of course does not follow.
kazinator 11y ago
The Halting Problem helps us prove programs because it informs us that some functions cannot be computed. This means that the requirement spec for some computations cannot be implemented. When we spot this problem in a requirement spec, we instantly know that its proposed implementation is an incorrect program, no matter what that program is. We don't have to look at a single line of code.
kazinator 11y ago
Here is something else: provably correct code can demonstrate unacceptable complexity for some input cases. We know from the proof that it will halt and the result will be correct: in 200 years on the given hardware. You have to add a time bound as a requirement specification to avoid this, or a constraint on the complexity (e.g. "the implementation must use no algorithm slower than quadratic time in such and such inputs").
wglb 11y ago
It would seem that Dijkstra, were he alive, would disagree with that. Check google for Proof of Correctness for Dijkstra's algorithm. Also, Knuth in TAoCP spends significant time proving his programs correct. Further, there is a compiler that is asserted to be proven correct: http://compcert.inria.fr/ http://compcert.inria.fr/ Now it is possible you are working with a different definition of "proved correct" than I am thinking.
dllthomas 11y ago
On a lighter note: http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html

by lutusp 11y ago

geofft 11y ago

That is a very common but incorrect misinterpretation of the halting problem. The halting problem says that there exist programs that cannot be proven correct; it says that for any property you want to prove computationally, no program can give you an answer for every last program. It doesn't say anything about "non-trivial" programs. In particular, if you write programs with awareness of the halting problem in mind, you can write extremely complicated programs that are provably correct. One straightforward way to do this is with a language that always halts. The proof assistant Coq is based on such a language, and it's powerful enough to write a C compiler: http://compcert.inria.fr/ http://compcert.inria.fr/ It is certainly correct that you can't stuff an arbitrarily vexatious program through a proof assistant and get anything useful on the other side. But nobody is interested in proving things about arbitrarily vexatious programs; they're interested in proving things about programs that cooperate with the proof process. If your program doesn't want to cooperate, you don't need an exact answer; you might as well just say "No, I don't care, I'm not trusting you."

pekk 11y ago
That is an incorrect misinterpretation of the posts you are responding to. If a programming language is Turing complete, then there is no way to prove that programs in that language halt in the general case (undecidable). The general case is important. It is not reasonable for a compiler which claims to detect halting to just bug out and refuse to compile certain valid programs. At best, people might still run a linting program which detects halting sometimes, but that flakiness is no good for the compiler. One of the implications of the halting problem is that a language in which all valid programs halt is not Turing complete. If you mean to say that you think programming's future is languages that are not Turing complete, just say so and then you can avoid delivering these condescending lectures to people who are operating under the reasonable assumption that future programming languages of general usefulness will be Turing-complete just like almost all the successful languages of the past have been.
- geofft 11y ago
  No, I don't believe that the future is languages that are not Turing-complete, mostly because halting is not the property most people care about. I believe that a large part of the future will be languages that are not Turing-complete, for applications where that's appropriate (e.g., C compilers) but not where it's not (e.g., interpreters). I also don't think that "well, that's how we've always done it" is a particularly compelling argument given how young the field of programming languages is. For instance, another wonderful example of requiring code to cooperate with the proof process is Google's Native Client. NaCl doesn't care about halting; what it cares about is that the code in question only accesses its own memory, or makes specific pre-defined calls into the supervising code. You can do this with hardware support (and they did, with segmentation, where available), but you can also do this with software support. The NaCl technique is straightforward. You're required to lay out your assembly so that every 32-byte alignment boundary separates instructions; you must insert NOPs as necessary. Any fixed read, write, or jump must be within an address within a mask (or to a predefined address in privileged code), and any computed read, write, or jump must be immediately preceded, within the same 32-byte block, by a mask operation on the relevant register. For data, the mask enforces that only data is accessed; for jumps, the mask enforces that the jump target is within the code area and also 32-byte aligned. Now you've proven a fairly complicated property of the code, that control flow never escapes to privileged code except at well-defined entry points. Doing so on arbitrary x86 would be impossible (unless you resort to binary translation), but this is a very minor modification to arbitrary x86, and a regular C compiler can be easily modified to emit it. The resulting restricted variant of x86 remains Turing-complete. And it is entirely reasonable for the NaCl verifier to say "Uh, what are you doing, please try again" if presented with code that is technically non-malicious but does not follow the rules. The NaCl verifier doesn't claim to detect malicious code (that's the antivirus problem, and unsolvable). It claims to take code that makes a specific promise about not being malicious, and verifies that property.
  - dllthomas 11y ago
    "halting is not the property most people care about" I agree that non-Turing complete languages are hugely interesting and likely to be more important as we go forward. But not for this reason. Most of the non-trivial properties people do care about can be used to tell you if a program is going to halt in a finite amount of time. Want an upper bound on memory? This program doesn't have one? Well, then it never halts. It has one? Well, then we know it halts or loops within 2^bits steps - run it for that many steps and you know which. I think non-Turing-complete will prove interesting because our programs are currently described in Turing complete languages, but run in more constrained contexts anyway. A program that always halts after running for 2^100 steps is not Turing complete. A program that halts if it tries to use more than 2^100 bytes of memory is not Turing complete. Applying these constraints in this way doesn't help us with analysis much, but it hints that we can probably find other ways to constrain our programs which won't get in the way of what we're trying to accomplish, and it's quite possible that some of those will let us build languages more amenable to analysis (and further possible that the gains in analysis will make up for a limited amount of getting-in-the-way).
Animats 11y ago
Right. This is a bogus complaint about proof of correctness. The way you prove halting is to find some integer measure for each loop (like "iterations remaining" or "error being reduced") which decreases on each iteration but does not go negative. If you can't find such a measure, your program is probably broken. (See page 12 of [1], the MEASURE statement, for a system I built 30 years ago which did this.) The measure has to be an integer, not a real number, to avoid Zeno's paradox type problems. (1, 1/2, 1/4, 1/8, 1/16 ...) On some floating point problems, with algorithms that are supposed to converge, proving termination can be tough. You can always add an iteration counter and limit the number of iterations. Now you can show termination. Microsoft's Static Driver Verifier is able to prove correctness, in the sense of "not doing anything that will crash the kernel", about 96% of the time. About 4% of the time, it gives up after running for a while. If your kernel driver is anywhere near close to undecidability, there's something seriously wrong with it. In practice, this is not one of the more difficult areas in program verification. [1] http://www.animats.com/papers/verifier/verifiermanual.pdf http://www.animats.com/papers/verifier/verifiermanual.pdf
- nickpsecurity 11y ago
  Pascal-F is interesting and not in my collection. What were most useful or interesting things you did with it? And does it have any use today in modern Pascal-like languages (maybe Modula-2 revision)?
lutusp 11y ago
> It doesn't say anything about "non-trivial" programs. No, but its source does. The source for the Turing Halting problem is Gödel's incompleteness theorems, which do specify that the entities to which it applies are non-trivial. The Turing Halting problem, and Gödel's incompleteness theorems, are deeply connected. > One straightforward way to do this is with a language that always halts. That doesn't avoid the halting problem, it only changes the reason for a halt. And it cannot guarantee that that program will (or won't) halt, if you follow -- only its interpreter. > In particular, if you write programs with awareness of the halting problem in mind, you can write extremely complicated programs that are provably correct. You need to review the Turing Halting problem. No non-trivial computer program can be proven correct -- that's the meaning of the problem. It cannot be waved away, any more than Gödel's incompleteness theorems can be waved away, and for the same reason.
- deleted 11y ago
  [deleted]
- geofft 11y ago
  > The source for the Turing Halting problem is Gödel's incompleteness theorems, which do specify that the entities to which it applies are non-trivial. The Turing Halting problem, and Gödel's incompleteness theorems, are deeply connected. Gödel doesn't say anything about "non-trivial" any more than Turing does. His first theorem is a "there exists at least one statement" thing, just like the halting problem. Like the halting problem, the proof is a proof by construction, but that statement is not a statement that anyone would a priori are to prove, just like the program "If I halt, run forever" is not a program that anyone would particularly want to run. So while yes, they're deeply connected, from the point of view of proving actual systems correct, it's not clear they matter. And neither theorem says anything about "non-trivial" statements/programs (just about non-trivial formalizations and languages). Gödel's second theorem is super relevant, though: it says that any consistent system cannot prove its own consistency. But that's fine. Coq itself is implemented in a Turing-complete language (ML), not in Coq. It would be nice if we could verify Coq in Coq itself, but since Gödel said we can't, we move on with life, and we just verify other things besides proof assistants. (And it seems to be worthwhile to prove things correct in a proof assistant, even without a computer-checked proof of that proof assistant's own correctness.) This is not waving away the problem, it's acknowledging it and working within the limits of the problem to do as much as possible. And while that's not everything, it turns out a lot of stuff of practical importance -- perhaps everything of practical importance besides proving the system complete in its own language -- is possible.

catnaroek 11y ago

Wrong. What Russell/Gödel/Turing/Rice/etc. tell you you can't do is write a decision procedure that checks arbitrary nontrivial properties of programs. In other words, if you first write a program and only then ask whether it is correct, you've already lost. Obviously, the solution is to stop writing arbitrary programs. As Dijkstra said long ago, we need to find a class of intellectually manageable programs - programs that lend themselves to being analyzed and understood. Intuitively, this is exactly what programmers demand when they ask for “simplicity”. The problem is that most programmers' view of “simplicity” is distorted by their preference for operational reasoning, eschewing more effective and efficient methods for reasoning about programs at scale.

jonahx 11y ago
Nice post. Can you clarify your last sentence? What do you mean by "preference for operational reasoning"? What's an example of the more effective methods for reasoning about programs at scale that you're contrasting this to?
- catnaroek 11y ago
  “Operational reasoning” means using execution traces (the sequence of states underwent by a process under the control of your program) to derive conclusions about the program. You can do it in your head, using a piece of paper, using a debugger, using strategic assertions, etc. By “more effective methods for reasoning about programs at scale”, what I mean is analyzing the program in its own right, without reference to specific execution traces. There are several kinds of program analyses that can be performed without running the program, but, to the best of my knowledge, all of them are ultimately some form of applied logic.
- klibertp 11y ago
  It's a guess, but I think GP uses "operational" as a synonym for "imperative". I think I encountered the term "operational semantics" in the context of Prolog programming. Denotational semantics is a term for a kind of semantics which are mathematically pure. IIRC Prolog has both operational and denotational semantics defined and they conflict. There's something about cut operator and tree pruning, but I read this long ago :-)

jahewson 11y ago

The Halting problem can already be solved for a non-trivial subset of programs, take a look at Microsoft Research's "Terminator" project: http://research.microsoft.com/apps/mobile/news.aspx?post=/en-us/news/features/terminator.aspx http://research.microsoft.com/apps/mobile/news.aspx?post=/en...

kazinator 11y ago
But the halting problem for a subset of programs isn't The Halting Problem, which is the question whether a UTM can exist to calculate any function, over its entire domain.
- dllthomas 11y ago
  The parent's wording was a little sloppy, but the point was that the grandparent was incorrectly using the Halting Problem to argue that you can't even do it for a meaningful subset of programs, which of course does not follow.

kazinator 11y ago

The Halting Problem helps us prove programs because it informs us that some functions cannot be computed. This means that the requirement spec for some computations cannot be implemented. When we spot this problem in a requirement spec, we instantly know that its proposed implementation is an incorrect program, no matter what that program is. We don't have to look at a single line of code.

kazinator 11y ago

Here is something else: provably correct code can demonstrate unacceptable complexity for some input cases. We know from the proof that it will halt and the result will be correct: in 200 years on the given hardware. You have to add a time bound as a requirement specification to avoid this, or a constraint on the complexity (e.g. "the implementation must use no algorithm slower than quadratic time in such and such inputs").

wglb 11y ago

It would seem that Dijkstra, were he alive, would disagree with that. Check google for Proof of Correctness for Dijkstra's algorithm. Also, Knuth in TAoCP spends significant time proving his programs correct. Further, there is a compiler that is asserted to be proven correct: http://compcert.inria.fr/ http://compcert.inria.fr/ Now it is possible you are working with a different definition of "proved correct" than I am thinking.

dllthomas 11y ago

On a lighter note: http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html