Hacker News new | ask | show | jobs
by Sharlin 938 days ago
Well, famously the halting problem is undecidable.

As a consequence (via Rice's theorem [1]), all nontrivial semantic properties of computer programs are undecidable. That is, there's no algorithm that can answer "does program x have property y?" for all programs, although obviously it's possible to prove propositions about many individual programs.

Because Turing completeness is a fairly low bar to clear, there are infamously a lot of systems that were not designed (or indeed designed not) to be Turing-complete but nevertheless turned out to be so [2]. As such, things like the Java type system is undecidable – in principle there exist Java programs that the compiler can neither reject nor accept.

[1] https://en.wikipedia.org/wiki/Rice%27s_theorem

[2] https://beza1e1.tuxen.de/articles/accidentally_turing_comple...