Instead of talking about the halting problem, you might want to invoke Rice’s Theorem:
All non-trivial, semantic properties of programs are undecidable [Wikipedia].
A semantic property of a program is one that depends only on its behavior, not on it’s syntax. So “it’s source code contains an even number of for-loops” is not a semantic property; “it outputs 7″ is. The two “trivial” semantic properties that the theorem are excluding are very trivial: the semantic property “true” that is by definition true for all programs, and the semantic property “false” that is by definition false for all programs.
I agree with your main point that the halting problem (and Rice’s Theorem) are overstated. While there exist programs that halt (or output 7) that can’t be proved easily in whatever proof system you’re using, they’re mostly bad programs. If your programs works but requires transfinite induction to prove that it works, you should rewrite it to be easier to prove correct. Or maybe you’re legitimately doing something very complicated.
We need to focus on proving the properties that the user is interested in, rather than the ones the compiler is interested in.
I think existing proof systems (e.g. Coq) already do this, unless I’m misunderstanding what you’re asking for?
For example, here’s a type signature that only says you’re getting an integer out:
Fixpoint mystery (n : nat) : nat
And here’s one that says you’re getting a prime out (for an appropriate definition of the prime type):
Fixpoint mystery (n : nat) : prime
If you care that mystery produces a prime number, you use the second signature and go through the trouble of proving that it produces a prime. If you don’t, you use the first signature.
You might object that while prime is optional, nat is not. You still have to prove that your program type checks and halts (modulo coinduction, which lets you express non-termination). But the alternative is a program that might crash, and if it crashes then it definitely doesn’t work! Or if you really want to allow it to crash, you can express that too. Have everything return an option, and propagate them up to the toplevel, and print “oops, something went wrong” if it gets there:
Fixpoint mystery (n: nat) : option nat
Tldr; there’s a lot of leeway in what you choose to prove about your program in a proof assistant.
Instead of talking about the halting problem, you might want to invoke Rice’s Theorem:
A semantic property of a program is one that depends only on its behavior, not on it’s syntax. So “it’s source code contains an even number of for-loops” is not a semantic property; “it outputs 7″ is. The two “trivial” semantic properties that the theorem are excluding are very trivial: the semantic property “true” that is by definition true for all programs, and the semantic property “false” that is by definition false for all programs.
I agree with your main point that the halting problem (and Rice’s Theorem) are overstated. While there exist programs that halt (or output 7) that can’t be proved easily in whatever proof system you’re using, they’re mostly bad programs. If your programs works but requires transfinite induction to prove that it works, you should rewrite it to be easier to prove correct. Or maybe you’re legitimately doing something very complicated.
I think existing proof systems (e.g. Coq) already do this, unless I’m misunderstanding what you’re asking for?
For example, here’s a type signature that only says you’re getting an integer out:
And here’s one that says you’re getting a prime out (for an appropriate definition of the
primetype):If you care that
mysteryproduces a prime number, you use the second signature and go through the trouble of proving that it produces a prime. If you don’t, you use the first signature.You might object that while
primeis optional,natis not. You still have to prove that your program type checks and halts (modulo coinduction, which lets you express non-termination). But the alternative is a program that might crash, and if it crashes then it definitely doesn’t work! Or if you really want to allow it to crash, you can express that too. Have everything return anoption, and propagate them up to the toplevel, and print “oops, something went wrong” if it gets there:Tldr; there’s a lot of leeway in what you choose to prove about your program in a proof assistant.