What does “Undecidable” mean, anyway

Practical value of theory and formalism

• Several commenters say studying automata, grammars, Turing machines, and type theory significantly improved their software engineering, especially for:
  • Seeing through abstractions (regex, parsers, CPUs) as simple underlying mechanisms.
  • Designing domain‑specific languages (DSLs) with explicit axioms and rules.
  • Doing program analysis (compilers, security), where undecidability appears routinely.
• Others report the opposite: theory of computation never felt relevant in day‑to‑day SWE, whereas concrete CPU walk‑throughs were helpful.

DSLs, DDD, and types

• One thread connects formalism to Domain‑Driven Design: define a precise glossary, find bounded contexts, ensure internal consistency, and mirror business change costs in code.
• DSLs are suggested as a way to encode domain axioms and relations for clarity and onboarding.
• Type theory is framed as turning “what data is” into structured classes and relations so programs themselves become data for a type system to reason about.

Turing machines vs real computers

• Long back‑and‑forth on whether Turing machines are “theoretical mumbo jumbo” or essential foundations.
• Some argue modern CPUs (or RAM machines, C abstract machine) are closer pedagogical models and easier to understand.
• Others insist TM, lambda calculus, FSMs, CFGs, etc. are still the right foundation for understanding what computation fundamentally is, even if not for teaching low‑level programming.

Clarifying undecidability and the halting problem

• Multiple commenters stress: undecidable ≠ “no algorithm for any instance”; it means no single algorithm correctly decides all instances.
• Emphasis that undecidability is about guaranteed termination on all inputs, not mere difficulty or huge runtimes.
• Several point out common confusions:
  • Finite‑state or finite‑memory systems are, in principle, decidable; halting undecidability requires unbounded memory.
  • A halting oracle could be used to build general theorem provers or classify proofs for many formal systems, but not for every conceivable theory.
  • Mixing undecidability (CS) with “really hard but decidable” problems like bcrypt cracking or chess is misleading.

Logic, constructivism, and independence

• A detailed subthread distinguishes:
  • CS “undecidable” properties of strings/programs.
  • Logical “undecidable/independent” propositions (e.g., continuum hypothesis, axiom of choice) relative to a theory like ZFC.
• Constructive vs classical mathematics: in constructive settings, decidability has real force; in classical math, excluded middle effectively treats every proposition as decidable “in principle,” even when no computation exists.
• Some note that many undergrads never see this logical background, making decidability feel like “black magic.”

Uncountability, diagonalization, and function space

• Several comments relate undecidability to Cantor’s diagonalization:
  • There are countably many programs but uncountably many functions string → bool, so “most” such functions are uncomputable.
  • Halting predicates and similar objects live in this larger, non‑program‑representable space.
• Busy beaver and small universal/independent Turing machines are mentioned as striking examples at this boundary.

Intelligence, AI, and limits

• Some speculate whether “intelligence” might eventually get a formal stratification similar to computation (complexity classes, hierarchies).
• Discussion on whether there’s an upper bound on intelligence and whether self‑improving AI singularity ideas might run into limits analogous to incompleteness or undecidability.
• Others caution that “intelligence” likely isn’t totally ordered and is multidimensional (different abilities, approximate reasoning).

Pedagogy and culture

• Observations that many CS students treat theory courses as hurdles rather than tools, then discard them, leading to poor intuition about what’s possible or impossible.
• A few instructors ask how to better motivate interest in theory; some answers point back to showing its role in requirements negotiation (recognizing inherently undecidable specs) and in building robust abstractions.