I don't really get the gushing over this post in the comments, it papers over entire fields of program analysis in a single breath. While I like Graydon and respect his point of view, this paragraph is hopelessly over-simplified.
> Conversely, languages that have a GC have unfortunately often not felt it necessary to bother having strong local reasoning support. Java for example has a GC and also uncontrolled mutable aliasing, so weak local reasoning and consequently more-challenging formal verification. If you write to an object in Java every other variable referencing that object "sees" the change, so any logical formula that held over all those variables might be invalidated by the write unless you use some fancy method of tracking possible write-sets or separating the heap.
First of all, there have been several languages that regions in their type system and are still backed by GC, so this is a strawman. Take, for example, Pony. Second, there is an entire field of pointer analysis and escape analysis that can and does infer uniqueness and reasons about whether two references can be aliases. Third, the whole point of static types is to slice apart the heap into independently non-aliasing parts using this technology called "classes" and "fields". We're not talking about JavaScript here, I think we should stop pretending like Java and C# and Scala and a bazillion GC'd languages don't have local reasoning about mutable state.
> ...there is an entire field of pointer analysis and escape analysis that can and does infer uniqueness and reasons about whether two references can be aliases.
You can't do this automagically in the general case, you really do need something much like separation logic. (And of course the Rust borrow checking semantics can be seen as a simplified variety of separation logic.)
Classes and fields don't give you completely local reasoning about mutable state, because class/object A can end up depending on the mutable state of class/object B. And class inheritance as found in Java adds all sorts of further complexity of its own, especially as programs evolve over time.
> First of all, there have been several languages that regions in their type system and are still backed by GC, so this is a strawman
Is it? He's not claiming that GC somehow makes it impossible to have strong local reasoning. He's just saying that, for whatever reason, the designers of most languages have made choices contrary to that goal. Which seems obviously true to me. Counter-examples exist of course but looking at the mainstream GC'd general purpose programming languages (Java, C#, Python, etc) it is true.
> Third, the whole point of static types is to slice apart the heap into independently non-aliasing parts using this technology called "classes" and "fields"
The whole point according to who? "Object-oriented" design means many things to many people and from what I understand the original idea was gesturing at something that we would now call the "actor model" which legitimately does try and carve up the heap into non-aliased, owned data structures which can only be mutated through message passing, but OO as it is actually implemented in the real world seldom even approaches those original goals. And languages like Java do nothing to prevent you from storing mutable references to the same object in multiple different objects. This is drawn out more eloquently than I am capable of doing in this post https://without.boats/blog/references-are-like-jumps/
Doesn't the answer depend on whether or not the map is being mutated by other threads concurrently?
To be fair, even in Rust that answer would depend on the specific map implementation - for example if the map internally held a lock to expose a thread-safe non-mut interface, there's a race between when you remove/insert and when you read the size. That suggests that the whole concept of local reasoning about mutable state gets pretty messy pretty quick unless you stick to very basic examples.
> Doesn't the answer depend on whether or not the map is being mutated by other threads concurrently?
Yes. To reason about here, you need to look elsewhere. Reasoning locally about your code doesn't tell you what happens.
> To be fair, even in Rust that answer would depend on the specific map implementation
I'm not convinced that Rust would disappoint here - this example is the essence of what Rust promises to do safely (well, that and GC-less GC). Per tfa:
> for a very, very long time the field has been held back by programming languages with too much mutable aliasing to be tractable.
> And Rust makes this better?
> Yes. Rust references are subject to the "shared-xor-mutable" rule
If you're reading and writing to your map, then no-one else is. It's the reward you get for pushing through the pain of lifetimes/ownership that other languages don't impose on you.
To be fair, I haven't touched Rust since the latest push for async programming... has it really just dropped 'share-xor-mutable' on the floor?
> If you're reading and writing to your map, then no-one else is. It's the reward you get for pushing through the pain of lifetimes/ownership that other languages don't impose on you.
I think you have failed to engage with the thrust of what I said - if the map is Sync in Rust, all bets are thrown out the window of your ability to reason locally about whether this piece of code works just by looking at this function - the map may be mutated between your mutation & read of the size by another thread.
> If you're reading and writing to your map, then no-one else is. It's the reward you get for pushing through the pain of lifetimes/ownership that other languages don't impose on you.
Only if you use mutable references. A lot of Sync code doesn't necessarily give you a mut reference to enforce that exclusion (e.g. lock-free data structures).
> To be fair, I haven't touched Rust since the latest push for async programming... has it really just dropped 'share-xor-mutable' on the floor?
Async has nothing to do with it & share^mut is still correct. I'm trying to highlight that with Sync you can lose that because the interfaces all become share even if they under-the-hood mutate in a thread-safe way.
Ah - the author does call out that Rust can’t do local reasoning perfectly. The other place it comes up aside from the Sync example I describe is RefCell which similarly lets you mutate from behind a shared reference thus also violating local reasoning. The author also describes why Rust deviated here (the niche Rust was moving into with systems programming often needs an escape hatch for some small amount of non-local mutability)
Correct, I'm just highlighting that there are gaps in Rust's ownership model where local reasoning fails. They're fairly narrow compared to other languages, but you do have to know about them.
> Conversely, languages that have a GC have unfortunately often not felt it necessary to bother having strong local reasoning support. Java for example has a GC and also uncontrolled mutable aliasing, so weak local reasoning and consequently more-challenging formal verification. If you write to an object in Java every other variable referencing that object "sees" the change, so any logical formula that held over all those variables might be invalidated by the write unless you use some fancy method of tracking possible write-sets or separating the heap.
First of all, there have been several languages that regions in their type system and are still backed by GC, so this is a strawman. Take, for example, Pony. Second, there is an entire field of pointer analysis and escape analysis that can and does infer uniqueness and reasons about whether two references can be aliases. Third, the whole point of static types is to slice apart the heap into independently non-aliasing parts using this technology called "classes" and "fields". We're not talking about JavaScript here, I think we should stop pretending like Java and C# and Scala and a bazillion GC'd languages don't have local reasoning about mutable state.