alt Hacker NewsI was thinking for implementing borrow-checker like rules for C but after I have seen what SMT solver can do I think it is not necessary to constrain the language in this way.
I was thinking for implementing borrow-checker like rules for C but after I have seen what SMT solver can do I think it is not necessary to constrain the language in this way.
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.