But (for convenience?), mathematicians/computer scientists use Turing machines/Lambda Calculus/(your favorite programming language) for most purposes instead to model things, even though they have these really peculiar undecidability properties.
FSMs also have undecidability: for each one there an infinity of programmes they can’t even run.
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).
FSMs also have undecidability: for each one there an infinity of programmes they can’t even run.
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).