Interesting.

In Hoare-type proof of correctness work, it's normal to work backwards from the proof goal (such as an assert statement) back upwards through the program, adding info about code that affects the variables in the assertion. This approach to borrow checking follows that model. You want some state at some point, and you work backwards to see if the preceding code gets you there. Makes a lot of sense for lifetimes.

The main problem with doing this inside a compiler is performance. You backtrack for each thing you need to prove, going through the same code more than once. I used to think that compilers should use more verification technology, but people start screaming about compile times.