Well, famously the halting problem is undecidable. As a consequence (via Rice's theorem [1]), all nontrivial semantic properties of computer programs are undec

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 https://en.wikipedia.org/wiki/Rice%27s_theorem [2] https://beza1e1.tuxen.de/articles/accidentally_turing_complete.html https://beza1e1.tuxen.de/articles/accidentally_turing_comple...