undefined | Better HN

0 pointsvoidmain8y ago0 comments

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.

0 comments

lisper8y 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

voidmainOP8y 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.

lisper8y 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?

2 more replies

j / k navigate · click thread line to collapse

0 comments

lisper8y 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

voidmainOP8y ago

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"

lisper8y ago

> you don't need a halting oracle to express and verify arbitrary properties in a static type system

> it will not type check

I'm pretty sure it would. Why do you think it would not?

2 more replies

j / k navigate · click thread line to collapse