| > I can see that you don't so I'll try to be clearer. For any given program one might choose there is no reason in principle why a competent computing scientist can't perform a semantic analysis for every statement and then deduce from that whether it is totally or partially correct. 'Correct'? In what sense? 'Correctness' and halting have little to do with each other. For example: def f(p):
p()
return 2
is 'correct' if the definition of f is to evaluate to two. But it's not clear it's ever going to halt (depends on haltingness of p).But that being said, actually no, there are many reasons in principle why a competent computer scientist would not be able to perform a semantic analysis for every statement and deduce from that whether the program will halt. > Obviously most programs in the set of all programs are too long for a computing scientist to read in a human life time, but that's another issue entirely. Irrelevant because even an immortal computer scientist would be unable to determine if the program halts. > This points to (but doesn't prove) the possibility that the human computing scientist isn't using a decision procedure to analyze (or construct) the program. The difference between a computer and a person (and I'm going to ignore all the various philosophies of consciousness) is that a human will 'arbitrarily' determine under what system he/she wants to operate, and thus can change axioms on the fly. of course, one could write a computer system that does this as well. It's really not obvious what you're saying here > About here is where I expect to see some misinterpretation of Church-Turing as somehow proving that everything, including computing scientists, is a Turing machine brought up. Oddly, rarely is the far more interesting Curry-Howard correspondence mentioned. Computer scientists may or may not be turing machines, but any deterministic procedure they follow can be encoded as a turing machine so your distinction is irrelevant. I'm not sure what Curry-Howard really has to do with this, but in general, for a theorem checker, you should make sure your proofs are total. |
Confident ignorance isn’t a good look. To help you out, here you go from the wiki[1]:
To be fair to your time and mine—I stopped reading your reply there based on the principle that nonsense follows nonsense, so you needn’t elaborate further.[1] https://en.m.wikipedia.org/wiki/Correctness_(computer_scienc...