Tree Borrows

plf.inf.ethz.ch

562 points by zdw a day ago


kibwen - a day ago

Recent blog post from Ralf Jung providing some extra context: https://www.ralfj.de/blog/2025/07/07/tree-borrows-paper.html

Bonus: recent talk from Ralf Jung on his group's efforts to precisely specify Rust's operational semantics in executable form in a dialect of Rust: https://youtube.com/watch?v=yoeuW_dSe0o

jcalvinowens - a day ago

> On the one hand, compilers would like to exploit the strong guarantees of the type system—particularly those pertaining to aliasing of pointers—in order to unlock powerful intraprocedural optimizations.

How true is this really?

Torvalds has argued for a long time that strict aliasing rules in C are more trouble than they're worth, I find his arguments compelling. Here's one of many examples: https://lore.kernel.org/all/CAHk-=wgq1DvgNVoodk7JKc6BuU1m9Un... (the entire thread worth reading if you find this sort of thing interesting)

Is Rust somehow fundamentally different? Based on limited experience, it seems not (at least, when unsafe is involved...).

pvg - a day ago

The Stacked Borrows mentioned had threads in 2020 and 2018

https://news.ycombinator.com/item?id=22281205

https://news.ycombinator.com/item?id=17715399

chombier - 16 hours ago

The PLDI talk is also available: https://www.youtube.com/watch?v=CJi_Fcs4bak

nixpulvis - a day ago

Here's the implementation in Miri for those interested: https://github.com/rust-lang/miri/tree/master/src/borrow_tra...

vollbrecht - a day ago

Hmm i just tested out the claim that the following rust code would be rejected ( Example 4 in the paper).

And it seams to not be the case on the stable compiler version?

  fn write(x: &mut i32) {*x = 10}
  
  fn main() {
      let x = &mut 0;
      let y = x as *mut i32;
      //write(x); // this should use the mention implicit twophase borrow
      *x = 10; // this should not and therefore be rejected by the compiler
      unsafe {*y = 15 };
  }
Voultapher - a day ago

Amazing work, I remember reading the Tree Borrows spec? on Nevin's website a couple years ago and being thoroughly impressed by how it solves some pretty gnarly issue quite elegantly. And in my experience [1] [2] it does indeed allow for sensible code that is illegal under Stacked Borrows.

[1] https://github.com/Voultapher/sort-research-rs/blob/main/wri... Miri column

[2] https://github.com/rust-lang/rust/blob/6b3ae3f6e45a33c2d95fa...

fuhsnn - a day ago

I wonder if Rust or future PL would evolve into allowing multiple borrow checker implementations with varying characteristics (compile speed, runtime speed, algorithm flexibility, etc.) that projects can choose from.

wavemode - a day ago

From the paper:

> The problem with unsafe code is that it can do things like this:

    fn main() {
        let mut x = 42;
        let ptr = &mut x as *mut i32;
        let val = unsafe { write_both(&mut *ptr, &mut *ptr) };
        println!("{val}");
    }
No it can't? Using pointers to coexist multiple mutable references to the same variable is undefined behavior. Unless I'm just misunderstanding the point they're trying to make here.
pil0u - a day ago

Just realised that one of the author, Neven Villani, is Cédric Villani's (Fields Medal 2010) son. Apples don't fall far from the tree, indeed.

gavinhoward - a day ago

This looks excellent. I will probably implement this model for my own language.

- 17 hours ago
[deleted]
Nurbek-F - a day ago

It can't be a dejavu. I keep seeing this post every 2-3 months...

b0a04gl - a day ago

[dead]

olddustytrail - a day ago

_Tree Borrows_

"I want my fuckin' money back."

"Hoom, hmm, let us not be hasty!"

"You got 48 hours to deliver or the sapling gets it, Treebeard."