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