The original computer assisted proof of the four colour theorem was written in IBM 370 assembler [0]. This was naturally susceptible to programming errors such as those discussed above. Gonthier's subsequent certified proof requires trust in a much smaller body of code and hardware [1].
That's a really good question. I may have known the answer to it twenty years ago, but I don't now. XD
What I can tell you is that it wouldn't have been so straightforward as that. We're not talking about an axiom-to-result symbolic proof piece of software like you might attempt to write now. It wasn't a computer proof so much as a computer-assisted proof. Lots of human analysis to describe specific properties, and then a computer program to check that a long list of geometric configurations had those properties.
I don't know exactly what the program output as its proof, but I can only imagine the problems would have been small assumptions built into its design failing in corner cases. The theorem is notoriously difficult to reason about rigorously, and there have been a number of accepted proofs over the years that turned out to be false. It really doesn't help the whole situation that not only is it the first major computer-assisted theorem, it just happens to deal with a result that people are already wary of.
