All non-trivial semantic properties of a program are Undecidable.