You're right, I wasn't thinking about it clearly enough, and explained myself poorly. Let me try again.
I guess what I'm thinking about is more along the lines of what I messaged you about privately earlier; if we had a formal IR, then we could use it as the hub of a hub and spoke of language definitions. We could define Rust (and any other language) in terms of this formal IR (FIR). Compiling would be Rust -> FIR -> LLVM IR. Proofs could be done using the FIR, but actual compilation would be done via LLVM IR. The mapping between FIR and LLVM IR would have to be constantly maintained to deal with any changes in definitions of the LLVM IR, but assuming that the FIR was designed properly, it wouldn't change.
The issues with this are obvious:
- What, yet another IR‽‽‽
- Is it actually possible to capture all the concepts we need in a formal IR?
- Would it be more useful than just trying to use a theorem prover directly?
- What happens if the LLVM IR shifts such that we can't represent a concept in the FIR? Is it possible to extend it without breaking it?
- etc., etc., etc.
I don't know the answers to any of those; the only thing that I know is that proving things on a shifting and ambiguous foundation doesn't really work.