There are bugs found in programming language implementations all the time. I guess you are switching to machine code, good luck.
If we treat each human as a compiler of natural language, and there is enough ambiguity that each human arrives at a different result. Then is it really a proof?
[Citation needed]
2 + 2 = 5 -> Error
Every time.
The environment does matter. I think in your original objection, you were executing the code in different environments.
https://cs.stackexchange.com/questions/38152/what-is-determi...
And to the point of the original article. Each human interpreting natural language is a new environment. Each brain is a new compiler with different outcomes. Thus the ambiguity. Natural language isn't concrete enough to always have the same result when processed by different humans, or AI.
> the answer with many multi-threaded programs is often "no."
Isn't the original point, that natural language isn't sufficient for proofs? Aren't you agreeing now?