Limitations and Evolution

Limitations and Evolution

I think that's not so much a consequence of Rice's theorem as an effect of not supporting quite all of the sorts of constraints programmers use. A bigger issue is that, even for decidable questions of interest (e.g., is there a proof of the correctness of this code which would fit on a single page?) they're often NP-complete. So you get code with a comment explaining why it's okay, and programmers can check that it's true in polynomial time, but the static checker can't come up with the correct rule in a reasonable time (and, of course, the original programmer came up with the constraint first and then wrote the code to obey it). But that's an issue of feasibility, not decidability. This can be made practical with annotations and assertions, although these have to be made acceptable to programmers by being sufficiently readable and writable (so the programmer can write them without much trouble, and so other programmers find them helpful in understanding why the code works).

And, of course, a static checker is only really useful when the number of cases it fails to complete which people can tell are okay is low enough that it can usefully flag as flaws everything that it can't prove.