Erann Gat <gat@jpl.nasa.gov> wrote:
+---------------
| Programs that do *anything* interesting are a miniscule fraction of the
| space of possible programs.  All the programs that will ever be written by
| all the beings in the Universe capable of writing programs is a tiny, tiny
| fraction of the space of all possible programs!  The game is not to fret
| over what may or may not be possible for arbitrary programs.  The game is
| to find programs that have properties that we care about.  There is no
| reason why provable termination should not be one of those properties. 
| Certainly neither Turing nor Chaitin provide any compelling reason.
+---------------

For one good reason: You can! That is, you *can* prove termination of a
*very large* class of "programs that have properties that [you] care about".
Just follow the discipline of writing your proof & program *together*, as
taught by Dijkstra in "A Discipline of Programming", or by David Gries in
"The Science of Programming" -- starting with the desired result at the end
and backing up step by step until you have proved that your program will
still work correctly (including handling "input errors") no matter what
initial conditions are (which include input data). At every single stage
in the development of your program, you use only forms which can be proven
correct (including termination) -- that old "precondition/postcondition"
stuff -- and you compose them to create larger forms using rules which
guarantee (more "preconditions/postconditions") that those proofs of
termination are not violated.  Voila! When you're done, you *know* your
program will terminate!! [Not only that, you know it will give the right
answers!]

As Dijkstra once said somewhere [*very* loosely paraphrased, I've forgotten
the exact quote], there are enough "interesting" programs that one can
write which can be proven to be correct to fill billions of lifetimes,
so why should one waste one's life writing *incorrect* ones?

[Partial answer: Writing provably-correct programs is hard work, and
requires thinking. Finding the proper preconditions for some loops
can be "hard mathematics" (though most are pretty easy). This group
knows better than most what "Joe Average Programmer" thinks about
hard math...]

-Rob

-----
Rob Warnock, PP-ASEL-IA		<rpw3@rpw3.org>
627 26th Avenue			<URL:http://rpw3.org/>
San Mateo, CA 94403		(650)572-2607