3 ms·

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

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.
    - seanwilson 9y ago
      > 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. There's ways around it (e.g. proving progress is always going to be made instead of termination) and there's a web server in Coq: http://coq-blog.clarus.me/pluto-a-first-concurrent-web-server-in-gallina.html http://coq-blog.clarus.me/pluto-a-first-concurrent-web-serve... > 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. Again, look at the sel4 project. It verifies the correctness of an entire OS showing that formal verification is powerful, practical and useful. Google for all the algorithms that have been formally verified with Coq, Isabelle and other proof assistants. Why do you think it would be common properties of interest wouldn't be provable? Do you think mathematicians have this issue (there's not a lot of difference when you have expressive enough types)? You yourself must have an intuition about why the properties would be true so you should be able to write a formal proof of that although it can be very challenging currently.
- voidmain 9y ago
  I intended the program to clearly have a type error on the last line, where the string "foobar" is assigned to a variable that has been declared to be of integer type. (In hindsight, I guess it is ambiguous whether the imaginary pseudo-language we are communicating in types variables, as most static languages do, or values, as most dynamic languages do, and in the latter case it would type check. I should have done something that is a type error in either case, like `x = x / "foo"`.) My intent was to show that even though the desirable property 'does not encounter type errors in execution' is reducible to the halting problem in general, and in this particular case, is reducible to a famous conjecture, static type checkers can calmly and soundly verify that programs have this property! They do so by verifying a strictly stronger property, necessarily rejecting some programs that have the desirable property but accepting only programs that have it. A dependently typed language which can express properties like termination does the same thing, rejecting some programs that terminate but accepting only programs that terminate. In particular, they will accept only programs where YOU provide them with (at least an adequate sketch of) a formal proof of the property. In general, when writing programs, we ought to develop at least a very informal argument for why they have the properties we want them to have. To the extent that they are correct, these informal arguments could be formalized. It's possible to imagine that with future technology, formalizing these arguments with the assistance of powerful tooling will actually be easier than reasoning about them informally, in the same way that you often find running and inspecting your lisp program easier than reasoning about it without assistance. As far as I know, neither computability theory or any other theoretical obstacle rules this out; it is just (perhaps far) beyond the state of the art. Perhaps you have mistaken me for an absolutist advocate of static typing or formal methods, which I guess is reasonable in the context of the thread. I'm not at all: I've experienced plenty of joy and pain (and bugs) in both static and dynamic languages, and have had more experience and success with advanced testing methods than with formal ones. At this moment, I'm writing a testing tool in a dynamic language! I just wanted to clear up a technical misconception, because I have seen fields held back before by widely misunderstood impossibility results. Happy lisping!
  - lisper 9y ago
    Sorry, I missed the last line of your rewrite. I think we actually agree here. Static typing can be useful. I just personally find the manner in which it is usually deployed to be unnecessarily annoying.

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.
  - seanwilson 9y ago
    > 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. There's ways around it (e.g. proving progress is always going to be made instead of termination) and there's a web server in Coq: http://coq-blog.clarus.me/pluto-a-first-concurrent-web-server-in-gallina.html http://coq-blog.clarus.me/pluto-a-first-concurrent-web-serve... > 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. Again, look at the sel4 project. It verifies the correctness of an entire OS showing that formal verification is powerful, practical and useful. Google for all the algorithms that have been formally verified with Coq, Isabelle and other proof assistants. Why do you think it would be common properties of interest wouldn't be provable? Do you think mathematicians have this issue (there's not a lot of difference when you have expressive enough types)? You yourself must have an intuition about why the properties would be true so you should be able to write a formal proof of that although it can be very challenging currently.
voidmain 9y ago
I intended the program to clearly have a type error on the last line, where the string "foobar" is assigned to a variable that has been declared to be of integer type. (In hindsight, I guess it is ambiguous whether the imaginary pseudo-language we are communicating in types variables, as most static languages do, or values, as most dynamic languages do, and in the latter case it would type check. I should have done something that is a type error in either case, like `x = x / "foo"`.) My intent was to show that even though the desirable property 'does not encounter type errors in execution' is reducible to the halting problem in general, and in this particular case, is reducible to a famous conjecture, static type checkers can calmly and soundly verify that programs have this property! They do so by verifying a strictly stronger property, necessarily rejecting some programs that have the desirable property but accepting only programs that have it. A dependently typed language which can express properties like termination does the same thing, rejecting some programs that terminate but accepting only programs that terminate. In particular, they will accept only programs where YOU provide them with (at least an adequate sketch of) a formal proof of the property. In general, when writing programs, we ought to develop at least a very informal argument for why they have the properties we want them to have. To the extent that they are correct, these informal arguments could be formalized. It's possible to imagine that with future technology, formalizing these arguments with the assistance of powerful tooling will actually be easier than reasoning about them informally, in the same way that you often find running and inspecting your lisp program easier than reasoning about it without assistance. As far as I know, neither computability theory or any other theoretical obstacle rules this out; it is just (perhaps far) beyond the state of the art. Perhaps you have mistaken me for an absolutist advocate of static typing or formal methods, which I guess is reasonable in the context of the thread. I'm not at all: I've experienced plenty of joy and pain (and bugs) in both static and dynamic languages, and have had more experience and success with advanced testing methods than with formal ones. At this moment, I'm writing a testing tool in a dynamic language! I just wanted to clear up a technical misconception, because I have seen fields held back before by widely misunderstood impossibility results. Happy lisping!
- lisper 9y ago
  Sorry, I missed the last line of your rewrite. I think we actually agree here. Static typing can be useful. I just personally find the manner in which it is usually deployed to be unnecessarily annoying.