The question came up of how one validated a proof involving computers. I've heard that this was not an abstract problem: programming bugs were found in the program but then it was shown that the bugs did not affect the result.

I'm not sure whether anyone has independently written and run a program to verify the output.

Cheers,
Ben