I do not know if the borrow checker and Rust's type system have been formalized. There are stacked borrows and tree borrows, and other languages experimenting with features similar to borrow checking, but without formal algorithms like Algorithm W or J for Hindley-Milner, or formalizations like of Hindley-Milner and problems like typability for them, I am not sure how one can prove the complexity class of the borrow checking problem nor a specific algorithm, like https://link.springer.com/chapter/10.1007/3-540-52590-4_50 does for ML.
I also am not sure how to figure out if the complexity class of some kind of borrow checking has something to do with the exponential compile times of some practical Rust projects after they upgraded compiler version, for instance in https://github.com/rust-lang/rust/issues/75992 .
It would be good if there was a formal description of at least one borrow checking algorithm as well as the borrow checking "problem", and maybe also analysis of the complexity class of the problem.
There isn't a formal definition of how the borrow checking algorithm works, but if anyone is interested, [0] is a fairly detailed if not mathematically rigorous description of how the current non-lexical lifetime algorithm works.
The upcoming Polonius borrow checking algorithm was prototyped using Datalog, which is a logical programming language. So the source code of the prototype [1] effectively is a formal definition. However, I don't think that the version which is in the compiler now exactly matches this early prototype.
EDIT: to be clear, there is a polonius implementation in the rust compiler, but you need to use '-Zpolonius=next' flag on a nightly rust compiler to access it.
Interesting. The change to sets of loans is interesting. Datalog, related to Prolog, is not a language family I have a lot of experience with, only a smidgen. They use some kind of solving as I recall, and are great at certain types of problems and explorative programming. Analyzing the performance of them is not always easy, but they are also often used for problems that already are exponential.
>I recommend watching the video @nerditation linked. I believe Amanda mentioned somewhere that Polonius is 5000x slower than the existing borrow-checker; IIRC the plan isn't to use Polonius instead of NLL, but rather use NLL and kick off Polonius for certain failure cases.
That slowdown might be temporary, as it is optimized over time, if I had to guess, since otherwise there might then be two solvers in compilers for Rust. It would be line with some other languages if the worst-case complexity class is something exponential.
> IRC the plan isn't to use Polonius instead of NLL, but rather use NLL and kick off Polonius for certain failure cases.
Indeed. Based on the last comment on the tracking issue [0], it looks like they have not figured out whether they will be able to optimize Polonius enough before stabilization, or if they will try non-lexical lifetimes first.
I could imagine you being correct about the borrow checking typability problem being NP-complete. Or an even worse complexity class. Typability in ML is EXPTIME-complete, a larger set than NP-complete https://en.wikipedia.org/wiki/EXPTIME https://dl.acm.org/doi/10.1145/96709.96748 .
I also am not sure how to figure out if the complexity class of some kind of borrow checking has something to do with the exponential compile times of some practical Rust projects after they upgraded compiler version, for instance in https://github.com/rust-lang/rust/issues/75992 .
It would be good if there was a formal description of at least one borrow checking algorithm as well as the borrow checking "problem", and maybe also analysis of the complexity class of the problem.