An exploration of an alias-based reformulation of Rust's borrow checker, proposed as an alternative to the Non-Lexical Lifetimes (NLL) approach. Instead of lifetimes corresponding to program points, regions are redefined as sets of loans (borrow expressions). The analysis is expressed as Datalog rules tracking subset relationships between region variables and loan requirements across the control-flow graph. Key innovations include liveness-gated constraint propagation, which allows accepting more valid programs (including a previously rejected loop pattern in issue #47680). A prototype passes the full NLL test suite. The post details the Datalog rules for subset, requires, killed, and error relations, and discusses how the causal structure of Datalog derivations could enable better error reporting.
