3 ms·

> My original objection was to the claim that a non-trivial program could be demonstrated to be "provably correct." This statement is false. For non-trivial pro

> My original objection was to the claim that a non-trivial program could be demonstrated to be "provably correct." This statement is false. For non-trivial programs, it contradicts the simplest and most easily accessible interpretation of the Turing Halting problem and Gödel's incompleteness theorems, both of which demonstrate that this is not possible. You don't need to solve the Halting problem (or find a way around Rice's theorem, etc.) to write a single correct program and prove it so. A-whole-nother story is if you want a decision procedure for whether an arbitrary program in a Turing-complete language satisfies an arbitrary specification. Such a decision procedure would be nice to have, alas, provably cannot possibly exist. To give an analogy, consider these two apparently contradictory facts: (0) Real number [assuming a representation that supports the usual arithmetic operations] equality is only semidecidable: There is a procedure that, given two arbitrary reals, loops forever if they are equal, but halts if they aren't. You can't do better than this. (1) You can easily tell that the real numbers 1+3 and 2+2 are equal. [You can, right?] The “contradiction” is resolved by noting that the given reals 1+3 and 2+2 aren't arbitrary, but were chosen to be equal right from the beginning, obviating the need to use the aforementioned procedure. 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. Typically, this is only possible if the program and the proof are developed together, rather than the latter after the former. This much math you need to know if you want to lecture others on the Internet. :-p

dllthomas 11y ago
Very good analogy! > but were chosen to be equal right from the beginning While this was almost certainly the case, it's sufficient for them to have been chosen so as to be decidably comparable.
- catnaroek 11y ago
  > it's sufficient for them to have been chosen so as to be decidably comparable. Indeed. :-)
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.

dllthomas 11y ago

Very good analogy! > but were chosen to be equal right from the beginning While this was almost certainly the case, it's sufficient for them to have been chosen so as to be decidably comparable.

catnaroek 11y ago
> it's sufficient for them to have been chosen so as to be decidably comparable. Indeed. :-)

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.