In any case, their model is a kind of generalization of Rust, in that it can accept a lot of programs that standard Rust cannot (it is intended to be used for assigning types to unsafe code as well as safe code).
I feel like there is a misunderstanding here on either your or my side that I should clarify (so sorry in advance for not contributing to the main story directly here, I'll keep it brief): My type system cannot assign types to unsafe code by type-checking. It is true that there are some programs I accept that the compiler doesn't (yet) accept (i.e. around non-lexical lifetimes), but the vast majority of unsafe code is not accepted by the type system, and that was never the goal. However, the type system is sufficiently small and formal that I can define the mathematical contract associated with each type. Then I can "assign a type to unsafe code" by manually proving that the code satisfies the contract. This is useful because it means that the type soundness theorem extends to code using the unsafe code at its given type. That's however not assigning a type to the code in the classical sense, i.e., these contracts are nothing a type checker could have any hope of checking against.
Coming back to the proposal at hand: First of all, at this point we plan to finish the type system we have and write a paper about it, just so that there is something there. Whatever is the solution to this problem, it'll probably not be in that first type system. But of course we may want to amend that later. 
Still, reading the blog post, one way of maybe dealing with this that would fit the existing framework fairly well came to my mind, and now I am wondering how close you think that is to your post, @nikomatsakis. I think this thought already lurked in my head when we previously talked about it, but it is much easier to express in your "two-phase borrowing" than it was in "borrowing for the future" or "two-phase lifetimes". Warning, very fresh thoughts ahead.
So let's look at this code again:
/* 0 */ tmp0 = &mut vec; // mutable borrow created here..
/* 1 */ tmp1 = &vec; // <-- shared borrow overlaps here |
/* 2 */ tmp2 = Vec::len(tmp1); // |
/* 3 */ Vec::push(tmp0, tmp2); // ..but not used until here!
So here we have a shared borrow to vec while a mutable borrow is active. That is, on its own, not even a new phenomenon, it can already happen in today's code via re-borrowing. The following is legal, after all:
tmp0 = &mut vec;
tmp2 = { tmp1 = &*tmp0; Vec::len(tmp1) };
Vec::push(tmp0, tmp2);
I feel like the restrictions for this pattern a pretty much the same as the restrictions you give for two-phase borrows (at least if we allow full NLL), if we just think of the "inactive" phase of the mutable borrow as being a sublifetime for which tmp0 is shared re-borrowed elsewhere. Clearly that shared re-borrow has to end before the next use of tmp0, and only read-only operations are allowed on it.
Of course, the key difference in the first block of code is that tmp1 is initialized from vec, not tmp0, which makes this a fairly strange form of re-borrowing (and we probably would not want to allow it for mutable re-borrows). And of course if tmp0 is based on a field of a struct, it may not be possible to re-write the code into above form. Still I am wondering whether there is some connection here between "not-yet-active" mutable borrows and "shared re-borrowed" mutable borrows.