> Rice's theorem states that all non-trivial, semantic properties of programs are undecidable.

Are people okay with the word "non-trivial" ? Is it even quantifiable?

We call a property non-trivial if there is a computable (partial) function that satisfies the property and another computable (partial) function that doesn't satisfy the property.

E.g. "returns 4 for some input" is a non-trivial property: the function 'f(x) = 4' satisfies it, while the function 'f(x) = 7' does not.

Non-trivial here means something specific (see the other reply), people say "non-trivial" in this context as an abbreviation of what it means, it's not a vague term that readers are asked to give an interpretation to.

Even the introductory paragraph on Wikipedia that I mentioned immediately defines it for the context: “A property is non-trivial if it is neither true for every computable function, nor false for every computable function.” I think that’s as rigorous as can be. (You’d have to look up the actual definition of “property”, “computable”, and “function” of course. “True” and “false” are probably obvious, however.)