4 ms·
You are incorrect. Your objection is like looking at a pen-and-paper proof that a program terminates and saying it is invalid because of the halting problem. If
by chrismonsanto 10y ago
You are incorrect. Your objection is like looking at a pen-and-paper proof that a program terminates and saying it is invalid because of the halting problem. If you want to read more about this subject, I recommend Adam Chlipala's "Certified Programming with Dependent Types": http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/
- twblalock 10y ago> Your objection is like looking at a pen-and-paper proof that a program terminates and saying it is invalid because of the halting problem. That is a true statement for any program that accepts input, strictly speaking. The halting problem is unsolvable.
- roywiggins 10y agoA one-state machine that immediately halts, will always halt, regardless of the input. The halting problem cannot be solved in general, but some programs can be proven to halt (or not halt). That's how the first few Busy Beaver numbers were found. For something more substantial: a correct program that implements a regular language recognizer will always halt eventually on any input, because it always makes progress and doesn't have any nonterminating loops. It consumes the whole input and stops. The hard part is proving you wrote it correctly, but that's what coq et al are for.
- chrismonsanto 10y agoNo, this is not true. Writing a program to check termination proofs is not difficult. Writing a program to construct termination proofs isn't possible in the general case. If someone hands you a formal pen-and-paper proof of termination it is quite possible to check it for correctness. Analogous statements are true for programming in a dependently typed language.