Sometimes, to install a program, you have a choice between compiling it yourself or downloading a precompiled binary. In theory (using a new programming language and a new compiler designed specifically for this), is it possible to generate a witness / certificate with the compiled binary such that checking the witness / certificate is very easy when compared to compiling things yourself, but ensures that the compilation indeed yields this binary ?
To avoid trivial answers, I'll specify things a bit more: The source language should contain ML, and the target language should be some realistic assembly language. The compiler should do many optimizations so that speed of the compiled program is comparable to that of OCaml, and in particular the compilation can not be just concatenating an interpreter and the source.
From what I've read, the longest thing in compilation is the optimizations. So my question is more or less: Can optimizations run much faster on a non-deterministic machine (in which case, we can use the witness to know which path to take on the real machine).