What does “Undecidable” mean, anyway

> if you're dealing with a proposition that either has a proof or a proof of its negation, you don't need a solution to the halting problem to find it, you are guaranteed to find it eventually by definition.

You don't know what situation you are in ahead of time, this is the point (my proposed algorithm terminates on all inputs, including independent statements). If you had a black box machine that could tell you whether a statement was independent or not then that would be just as useful, yes. But that's also an undecidable problem. Yet a halting oracle can be used to compute it!

The author is correct, you are simply misusing or misunderstanding standard terminology =)

An oracle for the halting problem can not be used to prove or disprove the Continuum Hypothesis within ZFC. No amount of bickering over terminology can change that fact. You can claim that such an oracle can be used to show that the Continuum Hypothesis is independent of ZFC and that's true and something I explicitly pointed out in my reply to you, but that's not a general theorem prover at that point, that's a theorem classifier for a specific formal theory (namely ZFC).

ZFC is not the end-all be-all of first order logic and it's certainly not even a particularly good choice of formal model for dealing with Turing Machines. Your halting oracle will not be able to do the same kind of theorem classification for other formal theories, namely those that do not have a recursively enumerable set of axioms. The most obvious example of such theories are second order theories, but even if you restrict yourself to first order theories, you have examples of such theories like True Arithmetic where your halting oracle won't be able to classify propositions since even though it's a first order theory proofs can't be enumerated in the same way that proofs can be enumerated in ZFC (or other first order theories with recursively enumerable axioms):

https://en.wikipedia.org/wiki/True_arithmetic

In general if the basis of your argument depends on nitpicking terminology, then that's a good sign you might not actually understand the fundamental concepts at play and are instead just regurgitating terms that you've heard from other people which is what I suspect you're doing here.

I work in programming languages research. Nobody uses Turing machines for anything. We do talk about decidability when it comes to certain things (type-checking, for instance), but that doesn't use Turing machines directly.

The lambda calculus comes up frequently, on the other hand, but it's used as a base from which we build minimal languages to demonstrate a novel concept. It's a nice theoretical framework around which to model a language abstractly, but essentially no major languages are actually implemented as extensions to the lambda calculus. (The notable exception is, of course, Haskell, but Haskell was explicitly designed in this way because it was intended as a sort of playground for programming languages research — see "A History of Haskell: Being Lazy with Class" from HOPL-III, 2007.) For example, Rust's region-based memory management descends from Cyclone, and iirc (it's been a few years) Cyclone was formalized as an extended lambda calculus, but nobody would suggest that becoming a contributor to the Rust language would require understanding the lambda calculus.

> I don't think Turing machines or Lambda calculus are even that far removed to call them completely theoretical. You can easily implement a few functions in lambda calculus that already resemble modern programming interfaces.

1. Whether your second statement is true is irrelevant to the first. The lambda calculus and Turing machines are theoretical devices. That's a statement of fact, not an indictment of utility. They're abstract machines used to reason about the theory of computation.

2. Your second statement is just false, actually. The pure lambda calculus doesn't have any kind of value other than anonymous functions; you need to get into, e.g., Church encoding to take them anywhere "useful", and that's pretty far removed from how actual language implementations work. If you go to the simply typed lambda calculus with some base types (integers and Booleans, for instance), okay, great, but you still are so abstract as to be sufficiently removed from actual implementations that the connections are not direct. Even Haskell, the most lambda calculus-y language out there, is actually based on System-F — which is like STLC but adds universal quantification over types, allowing for parametric polymorphism. And that's such a significant addition that most theorists are pretty quick to argue that Haskell is really a System F derivative rather than a direct lambda calculus derivative (though, of course, all computation can be derived in terms of the lambda calculus).