>There are many correct programs that the BC is unable to prove to be correct and therefore rejects them.
No. The borrow checker rejects programs that are definitely incorrect. It does not require that the program is correct.
That's a big difference.