[anyfoo]

I'm curious how you find it to be hand-wavy? I only vaguely recall the details of Rice's Theorem and its proof from University years ago, but does it not stand on some very rigorous formal foundation?

In fact, computability theory sometimes strikes me as one of the most rigorous fields, and aren't all of the hand-wavy sounding words in Wikipedia's first paragraphs of Rice's Theorem for example, in reality very rigorously defined as well?

[mkagenius]

> 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?

[saithound]

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.

[Rerarom]

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.

[anyfoo]

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.)