alt Hacker NewsIn 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?
Replies
mlindner • yesterday at 9:27 PM
You can't formally verify the soundness of something that inherently necessarily relies on hardware implementations that themselves could be faulty.
➕ show 3 replies
Note that the Lean kernel itself is not formally verified.