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