Valen's Memory Safety: A New Kind of Borrow Checking
19 points by Verdagon
19 points by Verdagon
Last time I read https://verdagon.dev/blog/group-borrowing I was convinced that this approach works for simple structs + arrays where all fields are public, but would quickly become unwieldy for anything requiring "path abstraction" like a binary tree or linked list. Wildcard paths solve this complaint, neat! (I did not read the golden spike articles)
Still a little nervous about "value invalidation" TOCTTOU for how this system deals with concurrency, seems shared-xor-mutable has a leg up there, but this is looking pretty nice for the single-threaded case.
Thanks =) Another thing that will help with path abstraction is "associated groups/paths", which are like associated types but for groups/paths.
I think invalidation will work well with concurrency. The more I implement it, the more I'm discovering that invalidation and normal borrow checking are actually kind of the same thing (the difference between them lies elsewhere). So I think it'll deal with concurrency the same way as normal borrow checking. Specifically:
I'm having trouble putting it all in english, but I feel like a key here is that if a function (or scope?) has no mut effects, then it's effectively taking an "immutable" reference. From that, all the normal shared-xor-mutable benefits apply.
If someone has a reference into some data that is currently being shared to another thread via structured concurrency, they won't be able to mutate it during the structured concurrency.
This is what I'm saying: that sounds eerily similar to shared-xor-mutable :P
It seems like one plan would be to:
mut effects inside themmut effects inside themmut effects without also being a mut effect externally.is that about right?
I love this!
Do you have a sense for how your approach relates to OxCaml's Modes?
I have a hunch that Ante's safe shared mutability is built on something morally equivalent to OxCaml's uniqueness mode*. I know that group borrowing is different from Ante's approach, but they're clearly related.
I'm still excited about OxCaml, but a bit less than I used to be. Modes are elegant, but the language keeps getting more of them, and I'm afraid all the different possible combinations are going to make the language too unwieldy.
*here's a quote from the docs:
Uniqueness is irrelevant for types that don’t contain any memory locations subject to overwriting
It reminds me of what Ante calls "shape-stable," which I think is the same thing as what you're calling "type-stable."