It's very interesting that he is strongly for the use of computation in math, but strongly against using computer logic systems to formalize proofs--see opinion #184. I'd love to hear other people's take on this.

I saw how pro-computational he is from the one time I heard him talk. One of his most repeated phrases was, "you write a little computer program...", meaning as a way to enumerate some set of objects or calculate the size of something.