This is a really common misconception, but all of the borrow checker's rules are necessary to fully verify the memory safety of single-threaded programs too. I

This is a really common misconception, but all of the borrow checker's rules are necessary to fully verify the memory safety of single-threaded programs too. It just turns out that mathematically proving GC-free code to be free of use-after-free and double-free errors is really difficult unless you disallow a lot of things.