[Znafon]

Isn't it one of the reason limiting the power of static analysis and force us to use dynamic analysis to get certain information about the correctness of our programs ?

[red75prime]

If the halting problem was merely NP complex, it would have still limited practical possibilities of static analysis.

[adrianN]

Eh, modern SMT solvers are very practical tools, as are solvers for Mixed Integer Linear Programs. NP-completeness doesn't mean that you can't solve most instances you care about in reasonable time.

[red75prime]

Yes. And the halting problem doesn't preclude static program analysis even if it works with only a subset of all possible programs.

[adrianN]

It looks like we're in perfect agreement then.