A New Way to Think About Borrow Checking (In Reverse)

Travel backwards in time, so that you already know the future Oct 18, 2026 — Have you ever had a weird idea, and then it worked, but you can't really believe it? That's what I'm feeling right now, about Valen's borrow checker. Because it travels backward through time. Or, to be less dramatic, it walks functions backwards, which is still very weird. Years ago, if you told me it would be good to iterate a function in reverse, I would have called you crazy. It turns out, there's actually some really good reasons to do this, and it's fairly common when you're doing e.g. optimization passes. 0 But I don't think anyone's done this for checking memory safety. If you want a really deep look into the world of borrow checking, read on! We're about to see some weird things. 1 This is a pretty deep under-the-hood look into borrow checking algorithms. If you want something epic and entertaining instead, check out my recent post on The Golden Spike, and Resurrecting the Vale(n) Programming Language! A New Way to Think About Borrow Checking (In Reverse) A weird kind of borrow checker ...and a weird, backwards implementation! Phase 2: Static Typing Phase 3: Static Grouping Phase 4: Safety Checking Another Example Why backwards? Reverse-Walking with Loops More towards Rust's borrow checker? That's all for now 0 Or destructor insertion, and now, checking memory safety! 1 0% of this article was written by AI. More thoughts here. My stance: if you want someone to take the time to read something, take the time to write it by hand. Thanks for reading =) A weird kind of borrow checker This isn't going to be your normal shared-xor-mutable borrow checking. This is Valen's borrow checker, the one that makes shared-xor-mutable optional, and can call into Rust functions with memory safety across the boundary. Valen is still very experimental. Many things have holes and sharp edges, and likely will until v0.1 comes sometime in February. The glorious months-long refactoring spree is already underway (hence this new borrow checker!). Feel free to check out the Valen repo and beware, here be dragons! 2 It's kind of like Rust's borrow checker, but it also has memory-safe mutable aliasing. If you want to know more about that, check out this post, though you won't need to understand that for most of this post. 2 Green dragons, specifically. ...and a weird, backwards implementation! Valen compiles a function in four phases: 3 It parses the function, turning source text into an AST. It does static typing, figuring out the type for every variable, argument, and expression. It does static grouping, where every reference knows what variable (or what part of what variable) it's pointing at. 4 It safety-checks the function, to make sure that a reference isn't used after it's invalidated. I'll explain all of this further below. The weirdest part is that #4 happens in reverse. It looks at the last statement in the function, and then walks backwards until it reaches the top of the function. This is weird because, as far as I know, it's the only borrow checker whose safety check goes backwards. 5 Further below, I'll explain why we're going backwards (hint: convenience, loops, and speed). But first, let's see how it works, and what it even means to go backwards. Let's skip phase 1, and start with phase 2. 3 There's also a secret fifth phase, where we calculate what attributes to send to LLVM to describe what operations might change what groups. But that's out of scope for this article. 4 It also figures out all the groups invalidated by any mut effects from any instructions. 5 For example: Rust (NLL and the current Polonius) does a constraint-solve for region inference, then a forward pass to check for conflicts. (Note that rustc does do a backwards scan to figure out where each variable is used, but its actual memory safety checks happen in a forward pass.) Vale's typing pass determines regions, then a later forward pass does region borrow checking to determine when it can safely skip run-time generation checks. (Vale's region borrow checker was actually fused with its instantiator/monomorphizer.) Valen's previous borrow checker did it like Vale too; its typing pass determines groups, then a later forward pass would check at every use that it was declared more recently than it was "invalidated". There are a lot of other borrow checkers out there, but I haven't heard of any doing their safety checks in reverse. If anyone knows of any, let me know! Phase 2: Static Typing The static typing pass will be familiar to some of you, it assigns types to variables. For example, it turns this program: exported func main() { let fuel = 5; let force = fuel; } into this program: exported func main() { let fuel i64 = 5; let force i64 = fuel; } This is pretty normal, lots of compilers do it. Compilers usually do this as a forward pass, walking from the top of the function to the bottom, figuring out types as it goes. We're going to do something similar but weirder in phase 3; phase 3 is going to do static grouping. Phase 3: Static Grouping 6 This is another forward pass, which figures out where each reference points to. For example, in this program: func print_first_fuel_cell(s &Ship) { let first_ref = &s.fuel_cells[0]; print_int(first_ref); } Static grouping figures out that first_ref is pointing in s.fuel_cells[]: 7 func print_first_fuel_cell(s &Ship) { // Static typing says: first_ref &int // Static grouping says: first_ref &int in s.fuel_cells[] let first_ref = &s.fuel_cells[0]; print_int(first_ref); } In other words, it's pointing to an int somewhere in the s.fuel_cells[] array. This information is now part of the variable's type. We'll be using this information in the next phase, which actually checks for use-after-free. 6 I'll probably start moving away from the term "group" soon, switching to "path" instead. Opinions welcome! 7 In V1's static grouping phase, it would also figure out when a reference was made. So for example, instead of &int in s.fuel_cells[], it would know that it was &int in s.fuel_cells[] from line 7.2. This was pretty awesome, we were literally smuggling time and space information into a variable's type. This new V2 version doesn't need to do that because it does a backwards scan, as we'll see next. Phase 4: Safety Checking This post is half for fun, but also to ask for feedback on the algorithm. I don't think anyone's done it this way before, and there might be a good reason for that. If you see any problems with this approach, please help me out by leaving a comment, so I can fix (or scrap!) the approach. 8 Now we can use everything Phase 3 calculated! This is the phase that checks for use-after-free. It does it with a backwards scan, as was foretold. Let's see it happen in a slightly bigger example: struct Entity { hp int; buffs []int; } func add_buff(self &Entity mut) { ... } func foo(e &Entity mut) { let buff = &e.buffs[0]; e.add_buff(); print_int(buff); } This program is doing a use after free, and we want the compiler to complain. First, I'll desugar it into a more explicit syntax: struct Entity { hp int; buffs []int; } func add_buff<g'>(self &Entity in g) mut(g) { ... } func foo<g'>(e &Entity in g) mut(g) { let buff = &e.buffs[0]; e.add_buff(); print_int(buff); } Now I'm going to add in some comments, all determined by the backwards scan as it goes. Further below, I'll explain what "DECLARE", "USE", and "MUTATE" mean. struct Entity { hp int; buffs []int; } func add_buff<g'>(self &Entity in g) mut(g) { ... } func foo<g'>( e &Entity in g // DECLARE e (group g) ) mut(g) { let buff = &e.buffs[0]; // DECLARE buff (group g.buffs[]) e.add_buff(); // USE e (group g) // MUTATE group g print_int(buff); // USE buff (group g.buffs[]) } The algorithm walks in reverse, from the end of the function to the start. As it scans upward, it looks for these events: When we USE a variable, add it to the pending list. When we MUTATE anything, ensure no variables in pending are invalidated. When we DECLARE a variable, remove it from the pending list. pending contains all of the things USEd below, that we hope to see DECLAREd above. We hope to never see a MUTATE to anything pending. I think the best way to think of this is that pending contains all variables that will be used at some point below/later in the function, and therefore should be valid until then. To really understand it, let's see it in action. First, we look at the last line: print_int(buff); // USE buff (group g.buffs[]) This is a USE, so we add it to the pending list. pending now has: buff (group g.buffs[]) Now, still going backwards, we encounter the line above it: e.add_buff(); // USE e (group g) // MUTATE group g We see the MUTATE so we ensure no variables in pending are invalidated. Specifically, we'll ensure that nothing in pending is pointing at anything under e. buff (group g.buffs[]) ... This matches! Show a compile error. Here's what just happened: buff was pointing at g.buffs[], which starts with the g we just mutated with add_buff. That means that buff is invalidated above the line where it's used, which is a use-after-free. So the compiler shows an error here. Huzzah! 8 First person to break it gets a prize! Another Example Let's see a correct program, so we can see the backwards walk encountering a declaration. Here's the same program, but with e.add_buff(); moved up, to be the first line in the function. struct Entity { hp int; buffs []int; } func add_buff<g'>(self &Entity in g) mut(g) { ... } func foo<g'>( e &Entity in g // DECLARE e (group g) ) mut(g) { e.add_buff(); // USE e (group g) // MUTATE group g let buff = &e.buffs[0]; // DECLARE buff (group g.buffs[]) print_int(buff); // USE buff (group g.buffs[]) } Like before, we start at the end, and get to this line: print_int(buff); // USE buff (group g.buffs[]) ...and see that it's a USE so we add buff to the pending list: buff (group g.buffs[])