Rice s theorem

A theorem stating that any non-trivial semantic property of programs is Decidability - we cannot automatically determine arbitrary properties about what programs compute (e.g., "does this function always return a positive number?"), which is why type systems must be conservative approximations.

A theorem stating that any non-trivial semantic property of programs is undecidable - we cannot automatically determine arbitrary properties about what programs compute (e.g., "does this function always return a positive number?"), which is why type systems must be conservative approximations.