alt Hacker NewsIIRC Rust's borrow checker analysis is more or less a subset of what SMT solving is capable of. It's "just" a question of tradeoffs made with respect to performance, complexity, precision, etc.
IIRC Rust's borrow checker analysis is more or less a subset of what SMT solving is capable of. It's "just" a question of tradeoffs made with respect to performance, complexity, precision, etc.
It is a really tiny and trivial subset of what model checkers can do. Model checkers can often prove memory safety of entirely unmodified C code. The problem is that this still runs into complexity problems and does not scale to non-toy programs. But this would also really be very far at the other end of the borrow checker that would require rewriting everything into a very specific form a borrow checker accepts.. IMHO a middle ground with some annotations is realistic and would be far more convenient than a borrow checker when supported by good tooling.