Earlier quoted context omitted.
The second bullet in the second section is overpromising badly. In fact there are many, many, many ways to write verifiably correct code that leaves no dangling pointers yet won't compile with rustc. Frankly most of the complexity you're complaining about stems from attempts to specify exactly what magic the borrow checker can prove correct and which incantations it can't.
A great teaching technique I learned from a very good match teacher is that when explaining core concepts, the simplified definitions don't need to be completely right. They are much simpler to grasp and adding exceptions to these is also quite easy compared to trying to understand correct, but complex, definitions at the beginning.
That bullet, at its most charitable, defines the "idealized goal" of the borrow collector. The actual device is much less capable (as it must be, as the goal is formally undecidable!), and "learning rust" requires understanding how.