If I am looking at some code which includes computation (by which I include function calling but also reference access which is sometimes trickily ignored as a computation) then I cannot assess the behavior of this code without knowing either (a) the computation is side-effect free and therefore has a mere value semantics or (b) it is not and can potentially be affected by or affect non-local parts of the code.

To hit case (a) I don't need a language which enforces purity, but I do need to know that everything "beneath" where I'm standing is pure. In this case, uncertainty, even tiny amounts of it, whittles away (a) entirely and leaves me in concern (b).

I'm not saying that global reasoning is bad or infeasible, but I am saying that lacking purity you cannot trust local reasoning until you isolate the pure fragment. For instance, you might state that (!x + !y) involves the global reasoning of what the values of (x) and (y) are but is local reasoning otherwise. I'd argue that actually local reasoning is destroyed until you refactor this code as

    let x_value = !x in
    let y_value = !y in
    (x_value + y_value)

I previously wasn't saying that "locally pure" code is preferable to globally reasoned code. I'm not completely certain that I would say that in all cases. I feel very confident though that it's (a) the right default and (b) something that should be used to a far greater degree than most code I see written which more or less demands global reasoning to do anything non-trivial at all.