> Here is this brilliant logical tool for reasoning about programs, in this case Hoare triples' descendent separation logic. Now let's figure out how we can keep our programmers from having to learn how to use it!

That's a good description of the Rust borrow checker, which is intended to be a sound analysis but a lot more restrictive than full separation logic.