> Almost any interesting property about programs is undecidable. It's only undecidable if the language makes it undecidable. For example, subject reduction is

> Almost any interesting property about programs is undecidable. It's only undecidable if the language makes it undecidable. For example, subject reduction is decidable in a type-safe language (EDIT: with decidable type checking, oops!), because the very definition of type safety means that typability implies subject reduction. Of course, not everything of interest can be made decidable in a general-purpose language, but the integrity of a language's basic abstractions should never be in question.