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 stron

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.