As a hard result, undecidability may be unimportant. Someone rarely wants to know whether a Gödel sentence is "true" or determine whether a program that referen

As a hard result, undecidability may be unimportant. Someone rarely wants to know whether a Gödel sentence is "true" or determine whether a program that references itself halts. But such theorems, by placing a theoretical, if contrived, limit, often seem to have a qualitative implication as well: namely that solving the problem in the general case, even if we manage to exclude pathological cases, is hard or even unfeasible. It seems consistent with the fact that there is no known algorithm for deciding whether a theorem is true, or for accurately and fully predicting the behaviour of arbitrary programs. As you said, that doesn't make formal methods useless. But it reframes the discussion away from trying to find a universal problem solver towards discussing tradeoffs (e.g. pushing the proof burden to the programmer, rejecting valid programs, or using imperfect heuristics).