4 ms·

> 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 arbitra

> 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.
  - lisper 9y ago
    > Why do you think it would be common properties of interest wouldn't be provable? Because proving all common properties of interest is tantamount to proving all interesting mathematical theorems. > Do you think mathematicians have this issue Yes, obviously. If they didn't they wouldn't have jobs. > it can be very challenging currently Yes indeed, and that is exactly my point. Humans just keep finding new and more complicated things to care about. Math doesn't converge.

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.
- lisper 9y ago
  > Why do you think it would be common properties of interest wouldn't be provable? Because proving all common properties of interest is tantamount to proving all interesting mathematical theorems. > Do you think mathematicians have this issue Yes, obviously. If they didn't they wouldn't have jobs. > it can be very challenging currently Yes indeed, and that is exactly my point. Humans just keep finding new and more complicated things to care about. Math doesn't converge.