3 ms·

This argument is incorrect. The "halting problem" is the problem of determining if an arbitrary program halts. It is not impossible to prove, and verify mecha

This argument is incorrect. The "halting problem" is the problem of determining if an arbitrary program halts. It is not impossible to prove, and verify mechanically, that a particular program halts. The state of the art is not up to proving every desirable property of every program that we would like to build. But that has nothing much to do with computability. And some extremely impressive things have been done, like the seL4 separation kernel, which has static proofs of, among other things, confidentiality, integrity, and timeliness, and a proof that its binary code is a correct translation of its source.

lisper 9y ago
> It is not impossible to prove, and verify mechanically, that a particular program halts. OK, let's put that to the test. Here is a particular program: let x = 6 let y = 3 while true: if y>x then halt if is_prime(y) and is_prime(x-y) then x = x + 2 y = 3 else y = y + 2 endif Can you tell me if it halts or not? > The state of the art is not up to proving every desirable property of every program that we would like to build. Isn't that exactly the same as what I said? > But that has nothing much to do with computability. What does it have to do with then? > some extremely impressive things have been done Yes, in some very particular cases. But note that even a proof of correctness is not a guarantee that the code is bug-free. http://spinroot.com/spin/Doc/rax.pdf http://spinroot.com/spin/Doc/rax.pdf
- voidmain 9y ago
  I think you have missed my point. I am not saying that humans are able to solve the halting problem! Nor am I saying that static verification is always better than testing. I am saying that you don't need a halting oracle to express and verify arbitrary properties in a static type system, because a static type system can and will reject programs that would not have type errors dynamically. If you write this program in a statically checked language: let x : int = 6 let y : int = 3 while true: if y>x then break if is_prime(y) and is_prime(x-y) then x = x + 2 y = 3 else y = y + 2 endif x = "foobar" I can tell you that it will not type check. And for the same reason, if you write the same program in a language that can express termination and claim that it terminates, the program will not type check until you have supplied a proof of (edit: the negation of!) Goldbach's conjecture in a form that the type system understands.
  - lisper 9y ago
    > you don't need a halting oracle to express and verify arbitrary properties in a static type system Replace the word "arbitrary" with "some" and I'll agree with you. There are some things a static type system will tell you. Some of those things are even useful things to know. But there are some things a static type system will not tell you, and cannot tell you, and some of those things are useful things to know too. Furthermore, the way static type systems are used in practice, they don't just tell you things. They will actually refuse to let you run the program unless it conforms to some preconceived notion of correctness that is built in to the type system. Personally, that's the part that rubs me the wrong way. It is sometimes useful to me to run a program even if I know that it has certain kinds of errors in it. > it will not type check I'm pretty sure it would. Why do you think it would not?
    - seanwilson 9y ago
      > I'm pretty sure it would. Why do you think it would not? Languages like Coq require you to prove a function halts before it will compile. Yes, for an arbitrary function it can be arbitrarily difficult or impossible to prove termination. In most cases though, termination proofs aren't that complex (e.g. "it halts because the collection gets smaller each recursive call"). Besides, you're argument is basically sounding like "because you can't prove all functions halt it's a waste of time proving any functions halt". See the sel4 OS for an impressive example of what formal proofs can do.
      - lisper 9y ago
        > Languages like Coq require you to prove a function halts before it will compile. Well, that's incredibly stupid. That means you can't write, for example, a web server in Coq unless you intentionally introduce undesirable behavior to satisfy the compiler. > because you can't prove all functions halt it's a waste of time proving any functions halt No. That's obviously a straw man. Can you please consider the possibility that I might not be a complete idiot? My argument is: because the halting problem is undecidable, there are an infinite number of properties of programs that are also undecidable. So there are only two possibilities: 1. None of the infinite undecidable properties of programs are things we will ever care about or 2. There are properties of interest that cannot be decided by static typing Which of those is the case is an empirical question but I submit that #2 is much more likely to be the case. Therefore, static typing cannot obviate the need to be prepared for your program to exhibit unexpected behavior at run time except in the most trivial cases.

lisper 9y ago

> It is not impossible to prove, and verify mechanically, that a particular program halts. OK, let's put that to the test. Here is a particular program: let x = 6 let y = 3 while true: if y>x then halt if is_prime(y) and is_prime(x-y) then x = x + 2 y = 3 else y = y + 2 endif Can you tell me if it halts or not? > The state of the art is not up to proving every desirable property of every program that we would like to build. Isn't that exactly the same as what I said? > But that has nothing much to do with computability. What does it have to do with then? > some extremely impressive things have been done Yes, in some very particular cases. But note that even a proof of correctness is not a guarantee that the code is bug-free. http://spinroot.com/spin/Doc/rax.pdf http://spinroot.com/spin/Doc/rax.pdf

voidmain 9y ago
I think you have missed my point. I am not saying that humans are able to solve the halting problem! Nor am I saying that static verification is always better than testing. I am saying that you don't need a halting oracle to express and verify arbitrary properties in a static type system, because a static type system can and will reject programs that would not have type errors dynamically. If you write this program in a statically checked language: let x : int = 6 let y : int = 3 while true: if y>x then break if is_prime(y) and is_prime(x-y) then x = x + 2 y = 3 else y = y + 2 endif x = "foobar" I can tell you that it will not type check. And for the same reason, if you write the same program in a language that can express termination and claim that it terminates, the program will not type check until you have supplied a proof of (edit: the negation of!) Goldbach's conjecture in a form that the type system understands.
- lisper 9y ago
  > you don't need a halting oracle to express and verify arbitrary properties in a static type system Replace the word "arbitrary" with "some" and I'll agree with you. There are some things a static type system will tell you. Some of those things are even useful things to know. But there are some things a static type system will not tell you, and cannot tell you, and some of those things are useful things to know too. Furthermore, the way static type systems are used in practice, they don't just tell you things. They will actually refuse to let you run the program unless it conforms to some preconceived notion of correctness that is built in to the type system. Personally, that's the part that rubs me the wrong way. It is sometimes useful to me to run a program even if I know that it has certain kinds of errors in it. > it will not type check I'm pretty sure it would. Why do you think it would not?
  - seanwilson 9y ago
    > I'm pretty sure it would. Why do you think it would not? Languages like Coq require you to prove a function halts before it will compile. Yes, for an arbitrary function it can be arbitrarily difficult or impossible to prove termination. In most cases though, termination proofs aren't that complex (e.g. "it halts because the collection gets smaller each recursive call"). Besides, you're argument is basically sounding like "because you can't prove all functions halt it's a waste of time proving any functions halt". See the sel4 OS for an impressive example of what formal proofs can do.
    - lisper 9y ago
      > Languages like Coq require you to prove a function halts before it will compile. Well, that's incredibly stupid. That means you can't write, for example, a web server in Coq unless you intentionally introduce undesirable behavior to satisfy the compiler. > because you can't prove all functions halt it's a waste of time proving any functions halt No. That's obviously a straw man. Can you please consider the possibility that I might not be a complete idiot? My argument is: because the halting problem is undecidable, there are an infinite number of properties of programs that are also undecidable. So there are only two possibilities: 1. None of the infinite undecidable properties of programs are things we will ever care about or 2. There are properties of interest that cannot be decided by static typing Which of those is the case is an empirical question but I submit that #2 is much more likely to be the case. Therefore, static typing cannot obviate the need to be prepared for your program to exhibit unexpected behavior at run time except in the most trivial cases.