@nprofile1q... SAT solvers are very complex, and would be even more complicated to prove them correct. Yet you can still formally verify that a particular solution is correct, if the SAT solver also emits a certificate along with the solution. This certificate can then be verified to be correct, and the verifier is small enough to be formally proven: https://www21.in.tum.de/~lammich/grat/. This doesn't mean that the SAT solver has no bugs, it may output a wrong result, but it'd be caught by the verifier.
Would a similar approach work for complicated compiler transforms? Instead of proving the implementation correct, you make it generate a certificate that can be used to check that the output is equivalent to the input. And you formally verify that verifier and run it as an additional compiler pass.
You don't need to prove the general case (that arbitrary pairs of programs are equivalent, which would run into the halting problem), or that the optimization implementation is always correct for all inputs. You'll only have proof that when called on your particular program the output is correct (which is what matters in the end?), and when the verification fails it'll output an internal error and refuse to produce output.
Has there been research in producing these certificates for compiler transforms?
Would a similar approach work for complicated compiler transforms? Instead of proving the implementation correct, you make it generate a certificate that can be used to check that the output is equivalent to the input. And you formally verify that verifier and run it as an additional compiler pass.
You don't need to prove the general case (that arbitrary pairs of programs are equivalent, which would run into the halting problem), or that the optimization implementation is always correct for all inputs. You'll only have proof that when called on your particular program the output is correct (which is what matters in the end?), and when the verification fails it'll output an internal error and refuse to produce output.
Has there been research in producing these certificates for compiler transforms?
1