Re: RA with MV attributes

Marshall <marshall.spight_at_gmail.com> wrote:
> In fact, if I understand
> Rice's theorem, *all* nontrivial properties of code
> are undecidable.

I'll be the picky person who points out that Rice's Theorem says all non-trivial properties of the (languages/problems/functions) that are (accepted/solved/computed) by code are undecidable. Clearly, the question "does this program use 'foo' as an identifier?" is both nontrivial  and decidable.

But yes, I agree with what you are ultimately saying. I'm being picky for the following reason. I would say that the distinction of properties of code versus its language/problem/function is relevant precisely because it explains that some kinds of analysis are possible in general even for a Turing-complete language, but they will just never correspond exactly to a property of the language. What can happen is that, for example, the failure of analysis to prove correctness doesn't NECESSARILY mean that a program is incorrect, but is a pretty damn good indicator in real life such that it would be a remarkable coincidence if the program actually were still correct.

-- 
Chris Smith