Can someone explain to me why decidability is of any practical interest at all? What's the (practical) difference between a decision procedure which might never terminate and one which might take 1,000,000 years to terminate? Actually, why push it out to 1,000,000 years: in the context of a compiler for a practical programming language, a decision procedure which might take an hour to terminate might as well be undecidable ... surely all we really need is that the decision procedure _typically_ terminates quickly, and that where it doesn't we have the means of giving it hints which ensure that it will.
I'm tempted to agree with you. I don't care if the compiler terminates on all my programs, or if it sometimes quits and says: "I don't know if this is correct." However, I do think that it is of very much importance that programmers and compiler implementors know which programs are legal and which are not. If a problem is decidable, it has the nice property that the problem (*not* the algorithm) can be used as a specification. Implementors are free to implement different algorithms, as long as they all solve the problem. If the problem is undecidable, how do you make sure that different compilers accept the same programs? If you don't want to find a subproblem that is decidable, you'll have to specify an algorithm, which is usually far more complicated, error-prone, and difficult to grasp for programmers. Cheers, Andres