[shasta]

Non-termination of some compiler inputs is a red herring. The only modification required to the original algorithm is that the search proceed in parallel (such that every input eventually makes arbitrary progress).

I agree with your point in a sister thread that decidable doesn't imply practical, but the claim of the original article was undecidable, which has a technical meaning.