You can go a step farther and model the instruction set and architecture, and which point you can make proofs about the final binary directly (thereby sidestepping the problem of compiler bugs). At this point, your assumption is just that your physical hardware actually matches your model.

Correct. It can happen, where the actual code, could diverge from a lean representation of it, in a glaring or subtle way.

You can do it backwards. You declare the properties you want the resulting program/function to have, using a proof assistant like Lean, then prove that a program exists that meets those requirements, and the proof assistant spits two things: a confirmation that the proof is valid, and a piece of code that implements the proof, in the form of computer code.

At least that's how the proof assistant Coq would often be used. You still have the challenge of ensuring that you have defined the properties you really want in the first place, but at least it solves the part where you want the code to meet the specification.

For things like programming languages we often have tedious, but slow, semantics that can be directly implemented in a suitable language. Then really all that a compiler or interpreter is is a faster version of those semantics.

If you are able to show correspondence between the fast and the the correct version, then you can toss the correct and slow version without even ever running it and just defer to the provably correct fast version.

Most software is ultimately like this