He's clearly not ignorant of computer assisted proofs, but I also wish he'd show more enthusiasm for them.
https://www.maa.org/external_archive/devlin/devlin_01_05.htm...
https://www.maa.org/external_archive/devlin/devlin_01_05.htm...
Homotopy type theory as a framework for doing proofs is exciting. Vladimir Voevodsky had a talk somewhere on youtube in which he claimed you could get similar length proofs in Coq using HoTT as you could on paper. He's also excited about the prospect of most math papers publishing machine-checked proofs.
I wish I could find the exact video for you.
Apparently the feels he can't be sure of the correctness of his own papers without machine checked proofs anymore, and he's a Fields medal winner:
I now do my mathematics with a proof assistant and do not have to worry all the time about mistakes in my arguments or about how to convince others that my arguments are correct.
But I think that the sense of urgency that pushed me to hurry with the program remains. Sooner or later computer proof assistants will become the norm, but the longer this process takes the more misery associated with mistakes and with unnecessary self-verification the practitioners of the field will have to endure
(from this http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundation...)
To answer gre's question, 1994 is the year Devlin cites a major breakthrough in the four color problem, in the very link that gre cited as an example of Devlin's lack of enthusiasm about machine checked proofs.
There are plenty of good reasons to mistrust machines when it comes to mathematical proofs, and mathematicians have been correct in their skepticism. Most of the work in Univalent Foundations has been directly aimed at addressing that skepticism. Optimism from its proponents in the 2010s is just as valid as the skepticism in the 70s and 90s.
And I mean just as valid in a very specific way; specifically in the spirit of the originally linked Devlin post published today.
(Check the link you cited; Devlin mentions 1976 and 1994 as key milestones for machine-checked proofs)
But HoTT and Coq are both still new, particularly when speaking of mathematics. When they figure out how to make LaTeX produce their textbook in a fully MathML-compatible fashion, then we can talk. :)