For completeness: Non trivial properties of programs are undecidable.