The reason decidability makes no or very little sense to tons of CS or Math majors is because the logical basis of decidability is almost never explained in school. Even if you're in a logic/computability class you likely won't get a very concrete explanation, unless you're in a Philosophy of Math class.
The problem that's usually not told to kids is that decidability has different sort of implications to classical mathematics and constructive mathematics. Since most undergrad programs only teach mainstream math (i.e. classical) and don't even mention constructive logic, decidability becomes a black magic situation for some confused students.
Here's the crucial part: decidability really only has material impact on our reasoning if we're in some kind of constructive setting. Undecidability does not and cannot have any impact on the results of classical mathematics, period, but it does have effect on the proofs of those classical theorems. It can also have impact on classical mathematics if we're reasoning classically but describing results in constructive settings (e.g. this is what happens when we do computability theory in classical mathematics).
In short, classically we're always allowed to work around undecidability by using an "oracle". But it can be important to state that we can only do it this way (similar to how we can state the need to use the axiom of choice).
One way to re-phrase Aristotle's law of excluded middle (forall P, P or not P) is to say: "every relation is decidable" which is how you would postulate it in homotopy type theory: https://agda.github.io/agda-stdlib/master/Axiom.ExcludedMidd...
This doesn't mean in classical mathematics every relation "literally" is decidable. Classical mathematics can still study constructive settings by creating a computational model (e.g. Turing Machine model). But it does mean that in classical mathematics every relation effectively is indistinguishable from decidable relations since given a statement like "Program P will halt" you are always allowed to say "either (program P will halt) or (program P won't halt)" regardless of our impossibility to prove one of the cases in general.
Also note that we call this kind of constructive reasoning "neutral constructive mathematics" which is when we operate in a constructive reasoning setting (like Agda's type theory above) but allow ourselves to say things like "AxiomOfChoice implies ExcludedMiddle" etc, read: https://ncatlab.org/nlab/show/neutral+constructive+mathemati...
I was with you until here:
> which is how you would postulate it in homotopy type theory: https://agda.github.io/agda-stdlib/master/Axiom.ExcludedMidd...
Why did you randomly shoehorn in homotopy type theory? Maybe I’m overreacting to this, but the only person I’ve ever known to shoehorn homotopy type theory into largely unrelated discussion has left quite a poor impression for me.
Why not? Why do you think it's irrelevant? The reason why I included that is very simple: it models the situation I want to express exceptionally well. In "mathematics" we learn in school none of the discussion relevant to the "Halting Problem" really is relevant, which is very confusing to students who even paid attention in school. To make the situation even relevant, we need to start assuming (or realizing, accepting, whichever one you want) that there are relations in mathematics that are undecidable. If you have a model of computation, which will internally be constructive, in order to freely apply our knowledge of mathematics onto this model, we need to go back to grade school and replace every instance of "is true" with "is constructible in your model of computation/programming language" (or more traditionally "is provable"). Which means you need an entirely different reasoning framework. So, to "go back" to classical math from having understood the existence of undecidability as "home", we need to unassume this, which will be identical to assuming all relations are "decidable" within your computational model. It's not like they actually are (at least not to the extent you can compute within). Homotopy theory is the exact thing that's developed to explain situations such as this one. Why not just use it? I apologize if anything I say is wrong or misleading, I'd be happy if you can clarify.