4 ms·

> mathematically you cannot prove all the properties of a program just by looking at its syntax, in general. A solution that is often overlooked is to simply s

> mathematically you cannot prove all the properties of a program just by looking at its syntax, in general. A solution that is often overlooked is to simply shrink the set of legal programs. Simply typed lambda calculus for instance has a perfectly decidable halting problem (which is, programs written in it always halt). There are 2 ways to handle undecidable properties with static analysis: either reject programs for which you can't prove the property holds (you will reject correct programs), or accept programs for which you can't prove it doesn't (you will accept incorrect programs, and may use runtime checks to compensate). Rejecting correct programs is a problem only to the extent one would like to write such a program in the first place. Take this expression for instance: if 2 + 2 = 4 then "Yay!" else 0 It is a perfectly fine expression, of type `string`. Most type systems will reject it however because the two branches of the conditional don't have the same type. Thing is, we don't care about this program in practice, since the constant test expression screams code smell to begin with.

gnulinux 9y ago
Yeah, but now you're arguing something else. Simply typed lambda calculus is not Turing-complete. With a Turing-complete language, you cannot decide the halting problem of an arbitrary sentence of that language. With a non-Turing-complete one, you potentially can. For example, Charity is one such non-Turing-complete language, for which, hypothetically, one can find an algorithm to decide halting of an arbitrary program. But most languages today are Turing-complete, because TC is a very easy property not to have, and it is very hard to construct non-TC but useful languages (eg, C++ metaprogramming is accidentally Turing complete, so is HTML+CSS). So, while what you explained is correct, it does not have direct implications on languages like Python, C++ etc. We still have different sort of properties while we're statically analyzing a TC language, and executing it with an input. This was what I was trying to explain.
- loup-vaillant 9y ago
  Being Turing complete doesn't mean you cannot prove anything without solving the halting problem. Programs have many potentially undecidable properties, and halting is only one of them. It's also one of the strongest. It doesn't matter which property you are looking at. If it's undecideable, you can sidestep the issue by forbidding programs for which the checker is not sure. That doesn't mean you have to lose Turing Completeness. You just have to chose properties that don't imply that the program halts. Static typing for instance doesn't mean the language isn't Turing Complete. Simply typed lambda calculus is the exception here.
  - gnulinux 9y ago
    Where did I claim "you cannot prove anything without solving the halting problem" or "static typing means non Turing complete" exactly? I said nothing of this sort... IN TC languages you can prove some properties, but in general you cannot prove your program is correct. When I say in general, I mean exactly that. You keep bringing some specific cases where you can prove correctness, but that's beyond my point. I sometimes workaround this by proving for "outputs the correct result, or loops forever". Here, you don't have to prove for halting, since your program is not expected to halt in some cases anyway. But then in some particular cases, you can prove that your algorithm is correct. You do not have to lose Turing-completeness to do this. But it gets trickier when you want to built a type system that can give all the bugs in your program, in general. You can definitely build something that finds all the bugs "for all intents and purposes" but not something that can be mathematically proven that will give you all of them. To be concrete, you can build a program, given arbitrary Python code, gives most of/all the bugs in this program. But you cannot build a program, given arbitrary Python code, that is proven that it will correctly know whether this program will output correct result for all possible inputs. You can do this for some restricted Python programs (as you've been arguing for last two comments) but in general you cannot do this, which brings us to this fundamental division.

gnulinux 9y ago

Yeah, but now you're arguing something else. Simply typed lambda calculus is not Turing-complete. With a Turing-complete language, you cannot decide the halting problem of an arbitrary sentence of that language. With a non-Turing-complete one, you potentially can. For example, Charity is one such non-Turing-complete language, for which, hypothetically, one can find an algorithm to decide halting of an arbitrary program. But most languages today are Turing-complete, because TC is a very easy property not to have, and it is very hard to construct non-TC but useful languages (eg, C++ metaprogramming is accidentally Turing complete, so is HTML+CSS). So, while what you explained is correct, it does not have direct implications on languages like Python, C++ etc. We still have different sort of properties while we're statically analyzing a TC language, and executing it with an input. This was what I was trying to explain.

loup-vaillant 9y ago
Being Turing complete doesn't mean you cannot prove anything without solving the halting problem. Programs have many potentially undecidable properties, and halting is only one of them. It's also one of the strongest. It doesn't matter which property you are looking at. If it's undecideable, you can sidestep the issue by forbidding programs for which the checker is not sure. That doesn't mean you have to lose Turing Completeness. You just have to chose properties that don't imply that the program halts. Static typing for instance doesn't mean the language isn't Turing Complete. Simply typed lambda calculus is the exception here.
- gnulinux 9y ago
  Where did I claim "you cannot prove anything without solving the halting problem" or "static typing means non Turing complete" exactly? I said nothing of this sort... IN TC languages you can prove some properties, but in general you cannot prove your program is correct. When I say in general, I mean exactly that. You keep bringing some specific cases where you can prove correctness, but that's beyond my point. I sometimes workaround this by proving for "outputs the correct result, or loops forever". Here, you don't have to prove for halting, since your program is not expected to halt in some cases anyway. But then in some particular cases, you can prove that your algorithm is correct. You do not have to lose Turing-completeness to do this. But it gets trickier when you want to built a type system that can give all the bugs in your program, in general. You can definitely build something that finds all the bugs "for all intents and purposes" but not something that can be mathematically proven that will give you all of them. To be concrete, you can build a program, given arbitrary Python code, gives most of/all the bugs in this program. But you cannot build a program, given arbitrary Python code, that is proven that it will correctly know whether this program will output correct result for all possible inputs. You can do this for some restricted Python programs (as you've been arguing for last two comments) but in general you cannot do this, which brings us to this fundamental division.