> 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

> 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/ https://without.boats/blog/references-are-like-jumps/