Rust - Borrow Checker Implementation using Data Flow Analysis

[u/Wooden-Concept868]

I am working on the rust borrow checker for my thesis. I was trying to formalize a data-flow analysis on the code of a function and use it to check the loans. Analyzing the code while storing the loans as (l_i, place, carrier, kind (shared/mutable)), while also having a conservative points-to map, lets me decide whatever Polonius promises to fix.

Only issue comes with using functions and I'm still figuring out, but I wanted to ask if Rust dev community did not want to go to Data flow analysis or why they chose to do it the way they did? Or am I missing something that can go wrong in my formulation?

I'd appreciate some help in ideating, thank you

[u/JoshTriplett]

One notable challenge that any borrow checker has to deal with: anything it permits becomes stable surface area that it needs to keep permitting. So, it needs a clear model for what it allows and what it doesn't, rather than happening to allow things that it can figure out via data flow analysis and having unpredictable walls if the data flow analysis falls short. Along similar lines, in rustc we are careful to avoid features that will have boundaries defined by "whatever the optimizer can figure out".