I do agree with the quoted statement. I have a lot of experience with machine-verified proofs (in a language called Coq). Even though Coq guarantees that an acc

I do agree with the quoted statement. I have a lot of experience with machine-verified proofs (in a language called Coq). Even though Coq guarantees that an accepted proof is correct, you still can't necessarily trust it, because your formal model of the program may be not accurate enough, or your statement of correctness is improperly stated. In this case, it seems like their proof was correct with respect to their model, but their model did not match up with reality. No amount of formalization will ever be able to solve this problem completely. I think the role of testing in this context is to make sure your formalization of the problem says what you meant to say about the world that you meant to refer to. Input/output examples (aka, tests) are a great way of convincing yourself of this.