3 ms·

Being Turing complete doesn't mean you cannot prove anything without solving the halting problem. Programs have many potentially undecidable properties, and ha

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

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.