I'm willing to consider that I might be wrong, but here's the argument.
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)
where the parenthetical fragment is now pure and local as the side effects were sidelined into the let clauses.
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.
First, I want to say that your last paragraph is something I do agree with. Sounds like we are ultimately on the same page and do actually agree with each other.
My point was simply that local reasoning is strengthened by trust in everything that you do locally. This is actually no different than living. I trust that what I hand off for recycling is actually getting recycled correctly. I have no real verification of this, however.
Now, you can work in a language that demands this for you. However, there are times where this demand actually makes things more difficult than they need to be. Conversely, there are plenty of times where not honoring this idea leads to annoyance.
Again, I do agree with your final point. I'm just not clear on where empirical results lie on this. Too much of it is just a very compelling argument.
I suppose I'm being a bit of pedant, but in my mind if you have to trust that some other actor (the recycling company) will do something then you're not actually talking about local reasoning but instead, exactly, global reasoning.
The local reasoning in this situation is you putting the refuse in the bin and placing it outside. All of that is "pure", completely in your control, and relies on exactly no side effects or outside state. It's also trivially testable, nearly failure proof, and completely observable. The "locality" of this implies that you need only consider exactly the things which are "in scope" at this moment and their behavior is entirely circumscribed by your "local" scope.
The moment you rely on an outside party whose capabilities rely on outside state then you lose all of those guarantees.
From a certain, high-enough level we can have "local reasoning" again in that the state of the municipal recycling service is encompassed. Or perhaps we also need to include the world oil supply in that model, who knows?
So, I'm being pedantic around the word "local reasoning". I think that's valuable because the kind of reasoning which is local is sharply distinct from that which isn't and it confers a lot of great properties. Finally, I'll reiterate, that I think side effects of any form utterly wreck local reasoning.
I get what you are saying. I was really just picking on the "absolutely" part of what you were saying.
Consider, I can absolutely use local reasoning to determine where trash should be to know that the truck driving by will pick it up and take it away. In that sense, I have done my small part and all decisions are locally reasonable. At a global scale, they may not be enough. And more measures may be needed, but not much breaks down on my doing my part.
Same for a program. I can reasonably be sure that calling println will not cause my machine to break, and will leave a note somewhere I can find it. Doesn't matter if this println is in the middle of a loop or not.
Heh, I just think you and I have different ideas about what "local reasoning" should mean. I cannot personally call your examples anything but very global.
Only when talking about the entire system. In which case, yes I fully advocate for more global reasoning. Above and beyond any considerations of purity, evidently. :)
Comments
I'm willing to consider that I might be wrong, but here's the argument.
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
where the parenthetical fragment is now pure and local as the side effects were sidelined into the let clauses.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.
First, I want to say that your last paragraph is something I do agree with. Sounds like we are ultimately on the same page and do actually agree with each other.
My point was simply that local reasoning is strengthened by trust in everything that you do locally. This is actually no different than living. I trust that what I hand off for recycling is actually getting recycled correctly. I have no real verification of this, however.
Now, you can work in a language that demands this for you. However, there are times where this demand actually makes things more difficult than they need to be. Conversely, there are plenty of times where not honoring this idea leads to annoyance.
Again, I do agree with your final point. I'm just not clear on where empirical results lie on this. Too much of it is just a very compelling argument.
I suppose I'm being a bit of pedant, but in my mind if you have to trust that some other actor (the recycling company) will do something then you're not actually talking about local reasoning but instead, exactly, global reasoning.
The local reasoning in this situation is you putting the refuse in the bin and placing it outside. All of that is "pure", completely in your control, and relies on exactly no side effects or outside state. It's also trivially testable, nearly failure proof, and completely observable. The "locality" of this implies that you need only consider exactly the things which are "in scope" at this moment and their behavior is entirely circumscribed by your "local" scope.
The moment you rely on an outside party whose capabilities rely on outside state then you lose all of those guarantees.
From a certain, high-enough level we can have "local reasoning" again in that the state of the municipal recycling service is encompassed. Or perhaps we also need to include the world oil supply in that model, who knows?
So, I'm being pedantic around the word "local reasoning". I think that's valuable because the kind of reasoning which is local is sharply distinct from that which isn't and it confers a lot of great properties. Finally, I'll reiterate, that I think side effects of any form utterly wreck local reasoning.
I get what you are saying. I was really just picking on the "absolutely" part of what you were saying.
Consider, I can absolutely use local reasoning to determine where trash should be to know that the truck driving by will pick it up and take it away. In that sense, I have done my small part and all decisions are locally reasonable. At a global scale, they may not be enough. And more measures may be needed, but not much breaks down on my doing my part.
Same for a program. I can reasonably be sure that calling println will not cause my machine to break, and will leave a note somewhere I can find it. Doesn't matter if this println is in the middle of a loop or not.
Heh, I just think you and I have different ideas about what "local reasoning" should mean. I cannot personally call your examples anything but very global.
Only when talking about the entire system. In which case, yes I fully advocate for more global reasoning. Above and beyond any considerations of purity, evidently. :)