Comment by lacker

In theory it would be possible to formally verify the soundness of the borrow checker. Maybe with AI advances we'll be able to do that in the near future. I mean, how much more complicated can it really be than proving Navier-Stokes?