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).
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).