3 ms·

> The way around the Halting problem is very similar: Don't write arbitrary programs. Rather, design your programs right from the beginning so that you can prov

by lutusp 11y ago

> The way around the Halting problem is very similar: Don't write arbitrary programs. Rather, design your programs right from the beginning so that you can prove whatever you need to prove about them. The system you outline works perfectly as long as you limit yourself to provable assertions. But Gödel's theorems have led to examples of unprovable assertions, thus moving beyond the hypothetical into a realm that might collide with future algorithms, likely to be much more complex than typical modern algorithms, including some that may mistakenly be believed to be proven correct. If we're balancing a bank's accounts, I think we're safe. In the future, when we start modeling the human brain's activities in code, this topic will likely seem less trivial, and the task of avoiding "arbitrary programs," and undecidable assertions (or even recognizing them in all cases), won't seem so easy. > This much math you need to know if you want to lecture others on the Internet. My original objection was completely appropriate to its context.

catnaroek 11y ago
> The system you outline works perfectly as long as you limit yourself to provable assertions. Of course. And if a formal system doesn't let you prove the theorems you want, you would just switch formal systems. > But Gödel's theorems have led to examples of unprovable assertions, thus moving beyond the hypothetical into a realm that might collide with future algorithms likely to be much more complex than typical modern algorithms, including some that may mistakenly be believed to be proven correct. Programming is applied logic, not religion. And a proof doesn't need to be “believed”, it just has to abide by the rules of a formal system. In some formal systems, like intensional type theory, verifying this is a matter of performing a syntactic check. > If we're balancing a bank's accounts, I think we're safe. I wouldn't be so sure. > In the future, when we start modeling the human brain's activities in code, this topic will likely seem less trivial, I see this as more of a problem for specification writers than programmers. Since I don't find myself writing specifications so often, this is basically Not My Problem (tm). Even if I wrote specifications for a living, I'm not dishonest or delusional enough to charge clients for doing something I actually can't do, like specifying a program that claims to be an accurate model of the human brain. > and the task of avoiding "arbitrary programs," and undecidable assertions (or even recognizing them in all cases), won't seem so easy. I don't see what's so hard about sticking to program structures (e.g., structural recursion) for which convenient proof principles exist (e.g., structural induction). Please, get yourself a little bit of mathematical education before posting your next reply. You're so stubbornly wrong it's painful to see.
geofft 11y ago
> If we're balancing a bank's accounts, I think we're safe. You seem to be contradicting your original claim, that it is impossible to prove any non-trivial program correct. Is this because you believe the program to balance a bank's accounts is trivial? Do you also believe that a C compiler is trivial? I guess we never defined what you meant by "non-trivial." If your position is that the vast majority of software in the world today is "trivial," sure, I'd agree with you. But that's not really a meaning of "trivial" that anyone expected.

by lutusp 11y ago

catnaroek 11y ago

> The system you outline works perfectly as long as you limit yourself to provable assertions. Of course. And if a formal system doesn't let you prove the theorems you want, you would just switch formal systems. > But Gödel's theorems have led to examples of unprovable assertions, thus moving beyond the hypothetical into a realm that might collide with future algorithms likely to be much more complex than typical modern algorithms, including some that may mistakenly be believed to be proven correct. Programming is applied logic, not religion. And a proof doesn't need to be “believed”, it just has to abide by the rules of a formal system. In some formal systems, like intensional type theory, verifying this is a matter of performing a syntactic check. > If we're balancing a bank's accounts, I think we're safe. I wouldn't be so sure. > In the future, when we start modeling the human brain's activities in code, this topic will likely seem less trivial, I see this as more of a problem for specification writers than programmers. Since I don't find myself writing specifications so often, this is basically Not My Problem (tm). Even if I wrote specifications for a living, I'm not dishonest or delusional enough to charge clients for doing something I actually can't do, like specifying a program that claims to be an accurate model of the human brain. > and the task of avoiding "arbitrary programs," and undecidable assertions (or even recognizing them in all cases), won't seem so easy. I don't see what's so hard about sticking to program structures (e.g., structural recursion) for which convenient proof principles exist (e.g., structural induction). Please, get yourself a little bit of mathematical education before posting your next reply. You're so stubbornly wrong it's painful to see.

geofft 11y ago

> If we're balancing a bank's accounts, I think we're safe. You seem to be contradicting your original claim, that it is impossible to prove any non-trivial program correct. Is this because you believe the program to balance a bank's accounts is trivial? Do you also believe that a C compiler is trivial? I guess we never defined what you meant by "non-trivial." If your position is that the vast majority of software in the world today is "trivial," sure, I'd agree with you. But that's not really a meaning of "trivial" that anyone expected.