I really like that we are now two posts deep from a quote from a ~1973 paper by Hoare. I posted a really long comment in the original boat’s article’s HN thread pointing out that skewing the quote towards a Rust-centric view (while understandable given boat’s history with the language) was an artificial narrowing of the scope of Hoare’s critique. Now Grayson has taken that narrow slice and used it as jumping off point to discuss a few interesting areas/design-points of Rust. While I still think my comment was correct, the ensuing discussion by Grayson in this blog were more than sufficient to overcome any technical gripes with the inciting article.
Since then, more advanced unsound methods than simple tests have only made unsound methods pull ahead of sound methods even further (I've posted other comments on this page to that effect).
Click on the timestamp in the comment (7 hours ago, or whatever). That'll take you to a page that has that comment as the root, so you can just copy that URL.
Hoare got so close. He found the problem, and in hindsight solving it using a type system to enforce shared xor mutability seems like a small step. Had he figured out that small step back was the solution back then he would have saved us 50 years of enormous amounts of pain.
My original comment about boat’s post citing the Hoare paper:
After the opening quote by Hoare and a quick intro paragraph, the author says 'What Tony Hoare was writing about when he said that references are like jumps was the problem of mutable, aliased state.' withoutboats is a well known Rust developer, so I guess this assumption about Hoare's quote should not be a surprise.
However, I don't see the text of the quote as reinforcing that perspective. I can see an argument for the article's extrapolation, taking Hoare's seemingly more general lamentations about the semantic existence of references (a semantic group containing at least 'reference, pointer, or indirect address into the languageas an assignable item of data') and then applying to the Rust model of non-aliased, mutable state as an attempt to circumvent the problems Hoare is addressing. But this argument is an attempt at taking a narrowly scoped perspective on a problem, correcting that small slice of the greater problem, and then announcing the entirety of the problem no longer exists. Like I said, understandable why the article would take this direction, I just don't think it truly addresses the totality of Hoare's critique of references as an undesirable semantic abstraction.
The title of the section withoutboats has quoted and the first sentence are unfortunately left out of his selection:
"8. Variables One of the most powerful and most dangerous aspects of machine code programming is that each individual instruction of the code can change the content of any register, any location of store, and alter the condition of any peripheral: it can even change its neighboring instructions or itself. Worse still, the identity of the location changed is not always apparent from the written form of the instruction; it cannot be determined until run time, when the values of base registers, index registers, and indirect addresses are known." [This paragraph is essentially acknowledging that low-level machine code gains its computational power from unlimited ability to alter the state of computation]
Also, the ... following the quote's second paragraph omits the following: "For example, in ALGOL 68, the assignment x : = y; always changes x , but the assignment x: = y+l; if x is a reference variable may change any other variable (of appropriate type) in the whole machine. One variable it can never change is x!" [This quote, which was removed, makes it explicit that Hoare is addressing the mere existence of references]
Both of the omitted sections tend very strongly toward Hoare's actual critiques being the semantic concept of references in high level languages being problematic, not merely mutable state. There is some natural extension of Hoare's discussion of references as means of assignment, which does lead to the 'spooky action' occurances. However, following this section of Hints on Programming Language Design, Hoare talks for a bit about structured programming, scope, and parameter importance. Discussing that without references, programmers have disjoint names for semantic objects and those are only altered/mutated by passing the sole existing object to a procedure as a parameter and having it passed back.
Overall, the TL;DR may be negatively stated as Rust developer gonna view things through a Rust-y lense. However, I think that is an incorrect reading. withoutboats skipped a crucial step in his going from Hoare's critique of referencs, they went directly from the text to an interpretation of the critique focused on aliased, mutable state. There is some discussion to be had about Hoare's assumptions of a single semantic object existing in a one-to-one correspondence with a disjoint source code name, especially in the context of multi-processor and networked programming prevalent in 2024. While I think that a more general solution to Hoare's problem exists and acknowledge Rust's attempts to at least tame a portion of the problem, I don't think any language has 'fixed' this issue.
> Both of the omitted sections tend very strongly toward Hoare's actual critiques being the semantic concept of references in high level languages being problematic, not merely mutable state.
Both sections however talk about mutations. Immutable references are not any different from inputs into a function.
