I'm well aware that it is unreasonable to expect the compiler to accept all safe programs, hence it needs to be conservative. It must only accept code that it c

I'm well aware that it is unreasonable to expect the compiler to accept all safe programs, hence it needs to be conservative. It must only accept code that it can prove to be safe or that is marked as unsafe (funny, maybe the keyword here should be safe, as the user vouches for the safety of the code) by the user. Your argument that for real world programs the borrow checkers conservatism does not create technical problems is completely plausible to me. The issue lies somewhere else. There is a psychological component to this. People struggle with the borrow checker, or at least they feel like they did. This is negative for rust. My point is that it would be better if it weren't trivial to write short, safe programs that are not accepted by the compiler. Where can one expect the line to be drawn? I don't know. I worked with Isabelle/HOL to formalize mathematical proofs and there I saw that we can indeed expect a computer to be reasonably clever in abstract reasoning. I'm not saying that the rust compiler is dumb, however, there is room for improvement. Thanks for your(plural) work on rust, btw.