alt Hacker NewsIt's fascinating that this kind of bug is exactly you can't really avoid even when rust is supposedly to guard against. Rust mitigated this problem a lot in practice, but you can never be certain because of issues like this in practice. This is similar that a math proof that's already been peer reviewed and accepted as truth, may still be possible to be wrong, although the chance is very small but it's not zero. Epseicially when the complexity gets higher.
Replies
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?
... and even if you formalize it, it could still be false due to an error in the theorem prover itself.
How is this different from any other compiler bug?
There was one in the Linux kernel a while ago that mistakenly eliminated an important null check.
Is this different?