Another way around the Rice's theorem is the Curry-Howard correspondence. A constructive proof of existence of a program that has a property can be transformed into a program that has this property. Yet another way is to have a programming language where syntactic correctness implies a range of semantic properties.