We investigate the precision of existing borrow-checking analyses; the current Non-Lexical Lifetimes (NLL) and future Polonius.
This is motivated by the exemplary program 'get_or_insert.rs', which is rejected by NLL, as it employs seemingly ordinary patterns that users might expect to function.
We aim to understand the current and future borrow-checkers of Rust and propose our own borrow-checking analysis on Rusts Mid-level Intermediate Representation, based on the classic compiler liveness analysis and encoding Rusts borrowing rules into overlapping borrow-expression.
With our proposed analysis follows a proof-of-concept implementation in Python which passes two accept cases currently rejected by NLL and rejects a trivially invalid program.
Out results are rebutted by unproven translation of NLL-rejected Rust programs into MIR and lack of correctness proof for our analysis.