Exactly. Static-analysis might be costly, but still can follow all possible paths. Just the proof of termination might be too hard - while (1) {...} -, or side

Exactly. Static-analysis might be costly, but still can follow all possible paths. Just the proof of termination might be too hard - while (1) {...} -, or side-effects are different, are but still the analyser must do its work. Same as a type checker, and on this analysis we must be able to rely on.