Fair enough. I must just not be understanding what the motivation for creating proofs of such software is then. I guess to me assuming the compiler or language runtime have no bugs seem to severely undermine the value of the proof. I feel like if the proof was to have value in an imperative language like C or C++ I would want the assembly proven, as the resulting computation can be drastically altered from the original source text between various compiler flags and optimization levels.