John Meacham wrote,
Again, I'm not sure that decidability helps practically here: we're not interested in "compiler A and compiler B accept the same programs", we're interested in "compiler A and compiler B accept some well defined subset of possible programs in a reasonable amount of time and space".
But it seems that well defining that subset is equivalent to the problem of finding a suitable decidable algorithm.
Fair comment. I was (unintentionally) playing fast and loose with terminolgy there. What I really meant by "well defined" in the above was much weaker than the context implied. I meant something more like "operationally useful and agreed on" in the way that most informal or semi-formal specs are. That's probably going to seem unsatisfactory to a lot of the readers of this list, and I guess I could reasonably be accused of begging Andres' question. But I stand by my original point. What I should have said in reponse to Andres' is that it's all very well, but most (or at least a very large proportion of) interesting problems are undecidable so, for those at least, the benefits of a decidable specification are moot. Expressive type systems, and programming languages in general, are a Good Thing, and I'm prepared to trade expressive power for decidability. Having a well understood and decidable fragment of such seems like a Good Thing too, it's just that I don't see many circumstances under which I'd need or want to restrict myself to working in that fragment. Cheers, Miles