Comment by zfnmxt | Hacker News Reader

Comment by zfnmxt | Hacker News Reader

Parent Full thread

> - Rice's theorem, that it is impossible to determine computational properties of arbitrary programs, will still apply, making static analysis (including antivirus programs, security scans, etc.) heuristic rather than exact.

I think this is misleading. There are many exact static analyses---proof-checking in theorem provers like Coq is an exact static analysis. More generally, type checking can be an exact static analysis that guarantees semantic properties of your programs, like termination.

If you can force your programs to be in a certain form (e.g., statically rejecting type incorrect programs), you can sufficiently restrict the class of programs (Turing machines) that you're considering that you can indeed determine non-trivial computational properties of your programs.

I was very careful to specify "computational properties" (as opposed to things like program length or side effects) and "arbitrary programs" (with "arbitrary" meaning that it doesn't suffice to prove individual programs correct, and "program" meaning that I'm not talking about single functions).

I should probably have been more specific by writing "decide" instead of "determine", because you can absolutely 'determine' a computational property as long as you're willing to ignore false negatives. For example, it's easy enough to write a termination checker by just checking for loops and equivalent constructs (or e.g. in Idris, by requiring that all functions are total), but that will of course reject a large number of programs that do in fact terminate.

Coq is not a Turing Complete language, so Rice's theorem doesn't apply. But almost all people are not writing programs in Coq.

I think static types are great, but they don't contradict any of this.

> but they don't contradict any of this.

Sure, and I agree with what you've said. But as you pointed out, you have to be very particular/exact with language with these things. I just wanted to emphasize that there are many constrained settings (but still practical) where Rice's theorem doesn't apply.

Reply on news.ycombinator.com