Isn't "code compiles" an insufficient criteria?
e.g you would need to prove that for all inputs the code produces the correct output which would in turn make the problem way more complex
e.g you would need to prove that for all inputs the code produces the correct output which would in turn make the problem way more complex