Comment by lacker
11 days ago
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?
Note that the Lean kernel itself is not formally verified.
Don't let the OpenAI marketing department hear you...
You can't formally verify the soundness of something that inherently necessarily relies on hardware implementations that themselves could be faulty.
You take hardware properties as axioms (for instance, ARMv6 cache coherency is specified in detail as part of the lengthy spec, even though you have no guarantees that the hardware actually is faithful to the spec)
You can certainly verify the soundness of what is within your control, the compiler code, which is what is being suggested above.
You can formally verify that the algorithm has the desired properties, though. If the hardware requires additional properties for soundness, then that would only be an error in the properties, not in the proof. (Of course, that would no longer prove soundness on that hardware.)
Just run it on open hardware.