I think the answer to this, if my experience as a maintenance programmer is worth anything, is: don't trust the prose. Trust the code (proof). This is why strong type systems are so insanely valuable in programming, especially if they encode proofs of side effects or lack thereof.

Maybe there's a sort of golden middle way here where all mathematical prose-proofs should be annotated[1] by the associated computer-checked proof. The trustworthiness of a particular proof could be assessed by the number of such references and how much coverage (of the prose) they provide...?

[1] Perhaps only by reference, as here. :)

EDIT: Quick edit, I say this as someone who -- earlier in xir career -- probably subjected a lot of people to somewhat verbose comments. In practice, my comments were usually right and the programming language wasn't powerful enough to capture the semantics of what I was doing. One hopes this is the distinction between good and bad comments. Sorry for veering off-topic.

Well I think you are talking about actual source code, and not the context of expository or academic writing. In that context, I would not trust comments even if companies had a strict policy of updating comments, because personally I just don't want to be susceptible to that.

It does make me wonder, though, about those computer-generated proofs which are so massive that no human can understand it. If you can run it...?

Hopefully, that won't be a problem with code written for a paper. You can freeze it then(for that version), unless errata is required.