I agree now and have changed my mind here (e.g. the Turing machine/equivalent formalism is “useful”). What changed it: I’ve since seen a few proofs by contradiction that were trying to show something impossible that I’d judge useful that were doing so by showing that you could decide something known to be undecidable, for example, decide whether ZFC is consistent (a contradiction assuming ZFC consistent).
Yes, I think in the real world there are these much more restraining concerns that undecidability does not (often?) become a real issue.
But it’s useful to know theoretically that you can’t solve a problem with any finite resources, because it stops you throwing resources at it.
I agree now and have changed my mind here (e.g. the Turing machine/equivalent formalism is “useful”). What changed it: I’ve since seen a few proofs by contradiction that were trying to show something impossible that I’d judge useful that were doing so by showing that you could decide something known to be undecidable, for example, decide whether ZFC is consistent (a contradiction assuming ZFC consistent).