Valen's Memory Safety: A New Kind of Borrow Checking

(verdagon.dev)

82 points | by verdagon 5 hours ago

15 comments

  • zamalek 9 minutes ago
    > Borrow checking has the "shared-xor-mutable" restriction: if you hold a reference to an object, nobody else can change the object.

    The article makes this sound like a problem. It isn't. This restriction frees you from thinking about certain classes of bugs in concurrent code; it's where the "fearless concurrency" comes from. R^w isn't about lifetimes - you could, in spirit (not sure about practice), remove it from Rust without affecting use-after-free at all.

    Of course, it means you can't write many completely valid programs, and so we'd hope there's a better solution, but removing it is not one.

    If you want to have to think about that (and potentially introduce bugs), that's perfectly fine. The flexibility of not requiring r^w is extremely useful. I'm just clearing up this mis-attribution.

  • melodyogonna 16 minutes ago
    Mojo's origin can represent a lot of these semantics. I think a lot was learned from Nick's proposal, even if it wasn't directly implemented. Here is an example of how you could represent the first snippet, where two references can update the same list: https://godbolt.org/z/78bhzWjYM
    • verdagon 1 minute ago
      Unfortunately, Mojo kind of limits itself by forcing all parameters to be unique references or shared references. So the first example works in Mojo, but not the rest of the examples.

      I hope they one day upgrade to full group borrowing, it would be a nice fit for them.

  • kvark 2 hours ago
    It sounds more like "path" borrowing than "group" borrowing to me, but the idea is great! Quite eye opening!

    One minor thing is that I'm not sure why they had to have "in" keyword for sub-borrows. Wouldn't it be more consistent to see "entity &world.entities[?]" instead of "entity in world.entities[]"? We'd consistently get the borrow "&" symbol and open the door for some contracts on what index (range) is affected.

    • cmrx64 45 minutes ago
      (hi kvark, long time!) it’s a clever algorithm, if you’re curious about other factorizations of referentiality frames I’ve been tinkering with analyzer across interpretation boundary like the gpu command queue :) I need to get some writing together. the techniques like from this post are a little “cute” compared to what real systems need.
  • Hunpeter 1 hour ago
    Off-topic (as I don't have the knowledge to intelligently comment on the concept): all I can think when I hear the name "Valen" is Babylon 5. I wonder if it's a coincidence or a deliberate reference?
    • variaga 44 minutes ago
      The about page says Valen is a successor to the Vale programming language, so I doubt it.
  • verdagon 5 hours ago
    Also, as I was writing this, a couple things occurred to me:

    * We _could_ use the function parameter syntax `entities: &world.entities[]` instead of `entities in world.entities[]`.

    * "Groups" aren't really central to understanding the idea, so Path Borrowing might be a better name than Group Borrowing.

    Opinions welcome =)

    • _old_dude_ 45 minutes ago
      Assuming “groups” are mainly about grouped invalidation, I agree, Path Borrowing is the better name, since it describes the core idea rather than the implementation mechanism.
    • munchler 3 hours ago
      FWIW `foo in bar` implies iteration to me, not a path. In the .NET world, for example, `bar` would be a collection that we’re iterating through, assigning each element to `foo` in turn.
    • scotty79 1 hour ago
      Love both.
  • amluto 1 hour ago
    Neat!

    I have a question about immutability. In Rust, if I have a shared reference to T (an &T a variable or a parameter), then I have a restriction that I can't modify T or anything in it (which Valen thinks is annoyingly restrictive, and I tend to agree), but I also have a promise that no one else will modify it. The latter is quite nice: it makes the optimizer happier (improves aliasing analysis), makes threading happier (nothing descended from the reference can have data races while the reference is alive), and makes me happier (I don't need to think about descendent values being mutated).

    Valen can call into Rust, and I think I can see how, at the site of any particular call, Valen can tell that no one is mutating the referent or its descendents: in a single-threaded world, the only thing executing is the current line of code or a maybe a few consecutive lines of code, and the compiler can see the function's signature and any mutable references therein, and if there is no permission to modify a descendent, then it doesn't get modified.

    But in a multithreaded world, especially if calling into Rust in a thread, doesn't there need to be a way to guarantee the immutability of an object across an entire region of code? How does that work in Valen?

    And for making immutability more comprehensible to people and to local analysis in general, would a special type of reference meaning "yes, this one really is fully frozen and there are no mutable paths into it for the entire lifetime of this reference" be a nice feature?

    (Aside: I've occasionally contemplated whether Rust would benefit from another flavor of reference: no-access. A no-access reference would guarantee the referent's existence but could coexist with shared and with mutable references. Safe code would be unable to read or write through such a reference. Other than making some cell-like types mildly less mind-bending, I'm not convinced I have an actual justification for this thing. This would give Rust three flavors of references.

    But I can imagine a Valen-like language having three flavors of references: frozen references (cannot use them to mutate and there's a promise that no one else can either), exclusive references (fully mutable, etc, just like Rust's &mut) and flexible references (the kind of reference in the blog post).)

  • peesem 3 hours ago
    nit: you need a better way of laying out asides/footnotes. when they get bunched up like at the start of this article you start having to scroll full screens back and forth. at least make the numbers on the asides link back to their position in the main text
    • Cpoll 2 hours ago
      They're fragment links, so you can use your browser's back button to go back to where you were.
    • verdagon 3 hours ago
      Yes, absolutely, lol. This article is really pushing my notes system past its limits. And it loops between six note colors, which normally isn't a problem, but is here. During the holidays, I want to see if I can implement Tufte notes like in https://edwardtufte.github.io/tufte-css/
  • giovannibonetti 3 hours ago
    I wonder if nowadays we should be focusing less on scalar data structures and more on languages that facilitate vectorized/SIMD instructions. Languages like Vx lang, Mojo, and Futhark that work both in the CPU or the GPU, although each one works in a different level of abstraction and control.
    • verdagon 3 hours ago
      GPU compilation is definitely something I intend Valen to support. I wrote about it back in 2022, [0] and I learned a lot of lessons on how to do it (and how not to do it!) from working on the Mojo compiler.

      The biggest decision for Valen is what to lower to:

      * Rust MIR, since rustc has CUDA now, [1] (perhaps other cards soon?)

      * SPIR-V, like Zig does for its GPU compilation [2]

      * MLIR

      Rust MIR is looking pretty nice. Valen already has Rust interop by doing some rustc sorcery, [3] and it would be somewhat straightforward to switch from emitting LLVM to emitting Rust MIR. I just need to figure out if Rust MIR can support the optimizations I have planned for Valen.

      In a perfect world, Rust would be able to lower its MIR to MLIR, since MLIR has so many backends. I recall there were some efforts to do that, unsure where that ended up.

      [0] https://verdagon.dev/blog/next-gen-languages-gpu

      [1] https://developer.nvidia.com/blog/introducing-cuda-rust-two-...

      [2] https://ziglang.org/devlog/2026/#2026-06-26

      [3] https://verdagon.dev/blog/golden-spike-reviving-vale-valen

    • 392 3 hours ago
      • cmontella 3 hours ago
        I don’t want to hijack Evan’s post by posting a link, but if you’re interested I’ve implemented many of the ideas in that presentation in the language I’m working on. You can check out the latest link in my post history for a rundown of how it works and a demo.
        • verdagon 3 hours ago
          Feel free to talk about it here, would love to hear about it!
  • c-fe 1 hour ago
    the link under recent posts here https://verdagon.dev/home 404s, as it links to https://verdagon.dev/blog/valen-memory-safety instead of https://verdagon.dev/blog/valen-group-borrowing . Interstingly this shows the page is hosted on Firebase, which is a bit unexpected for a static blog
    • verdagon 1 hour ago
      Should be fixed now, thanks!
  • maufl 3 hours ago
    How likely is it that such a borrow checker could be "backported" to Rust? Maybe in a new edition?
    • verdagon 3 hours ago
      You know, it's not crazy. Niko wrote about lifetimes based on places back in 2024, [0] though it was in the context of shared-xor-mutable, which is consistent with Rust's spirit.

      And Rust already supports forms of mutable aliasing already, such as with Cell, and GhostCell which is halfway towards Valen's approach. I would love to see someone augment GhostCell to have the sort of "invalidation" logic that group borrowing does. In fact, Plecra is working on something like that with their (WIP) "Exclusion Typing". [1]

      On top of that, Polonius already thinks in terms of "paths", just like Valen does. So it's not so much a question of compiler design, but of language design, and how Rust would expose it to the user.

      [0] https://smallcultfollowing.com/babysteps/blog/2024/06/02/the...

      [1] https://dilated.me/blog/posts/introduction-to-exclusion-typi...

    • zozbot234 1 hour ago
      It would have to take &Cell<T> references or the like in order to preserve the existing uniqueness properties for &mut T references. Not so different ultimately from what GhostCell, QCell, LCell etc. do already, except possibly simpler in some ways.
  • JackSlateur 11 minutes ago
    Checking the following code, could you confirm that is does not work concurrently ? The "world" var is read-only, does it mean that all other entities are also readonly (cannot be modified by another thread, for instance) ?

      struct World {
        entities Vec<Entity>;
      }
      func step(world &World, entity in world.entities[] mut) {
        entity.advance();
        let collision = world.get_collision_for_entity(entity);
        entity.resolve(collision);
      }
  • sebastianmestre 4 hours ago
    IIRC this Verdagon guy had a language called Vale... is Valen a rename or a new project?

    Edit: tfa makes it clear it's a separate project

    • verdagon 4 hours ago
      Hi! Kind of both. Even though Valen reuses 90% of the Vale compiler, its approach (Rust interop, borrow checking with mutable aliasing, etc.) is so different that it really needed a new name.

      Also, I really like where Vale ended up, Vale's generational references + region borrowing was a truly weird and unusual memory safety blend. I didn't want that combination to be lost to time, so I wanted "Vale" to keep referring to that.

  • user142 3 hours ago
    I noticed that there is no control flow in the examples.
    • verdagon 3 hours ago
      Next article =) How the borrow checker handles ifs and loops is a pretty fun topic. If-statements work like you'd expect (invalidations from both branches are merged). Loops is where it gets weird: we have to scout all the invalidations that happen inside the loop and then "replay" them _before_ the body of the loop. I can explain it more if you'd like.
      • user142 3 hours ago
        I was wondering about the case where a reference points to a different path depending on control flow. I guess you can just design your language to make this impossible but this is still possible to do with pointers in C/C++.
        • verdagon 2 hours ago
          Theoretically, we can have a reference that points to two paths, a "path union" so to speak. If the user explicitly typed out the path union, it would be something like:

          let my_ref &Entity in (live_list[], dead_list[]) = if ...

          though it would be nicer in practice, because the compiler could infer that.

          Haven't implemented it yet of course, but the data structures in the borrow checker are designed with this in mind.

          • eptcyka 1 hour ago
            Would it then be possible to mutably reference two entries in the same hashmap?
  • fithisux 3 hours ago
    Is it possible to retrofit it to Freepascal, D, Freebasic or even Java?
    • verdagon 3 hours ago
      Maybe! I think about D a lot when designing Valen, since they attempted to blend borrowing with garbage collection. Swift is facing some of the same challenges, and I expect Java could soon too now that Valhalla has landed.

      If Valen solves those challenges as well as I think it can, it could be a good direction for them to explore.

  • falconBrisk47 4 hours ago
    Path Borrowing reads clearer to me, "group" made me look for a group type.