I was interested in math and physics as a teenager and I became interested in logic as it seemed fundamental to these. In retrospect this may have been fortuitous; at least one of my math teachers thought it was a silly waste of time.
Gödel was already famous and I wanted to understand his work. I picked up a smattering of logic from several semi popular books plus a few standard sources.
I entered the University of California at Berkeley as a junior in 1953 a took a course in formal logic from Benson Mates where we covered essentially the material in Quine’s “Mathematical Logic”. We devoured that meticulously finding and fixing a proof or two in the process. Here is a recent note that I wrote in response to recent questions based mostly on what I learned from Mates. The final exam consisted of recapitulating Henkin’s completeness proof for first order predicate calculus. Here is what I took away from that course. After that I sat in on a couple of Tarski’s graduate logic courses but got only a smattering of the content. I did learn more about models.
Other concurrent math courses, and at least one physics course left me with the impression that most math and a little physics were susceptible to the rigor imposed by the formal methods, i.e. that formal methods were powerful enough. But should we, must we believe formally proved theorems?
After graduating in 1955 I went to Livermore and got my first access to a computer. I had written just a few programs before then but had not had the exasperating experience of a real computer finding all the nit-picking bugs. I had thought that my careful proofs that I produced as a student were near perfect. My confidence was badly shaken when the real rigor of a computer confronted my programs. The good news was that with the computer as a task master, I could actually debug my programs and either corroborate my original ideas or learn where those ideas went wrong. The computer was actually a new sort of way to learn new math and physics!
Shortly thereafter I had my first experience with a compiler where something akin to “well formed formulae” were read and critiqued by a computer. The idea was immediate that a program a bit like and simpler than a compiler could check formal proofs.
The computer did not help gain confidence in those beautiful proofs that I had built for subjects like Lesbegue measure or differential geometry. Indeed it shook my confidence in the correctness of those proofs I had written. Sometimes the computer merely shows you that you omitted a comma. Other times it show you that your idea is no damned good.
I did learn to believe the ability of a computer to compute the sum of a large number of numbers, despite the fact that computers of that day made many errors. The sorts of error that computers made are very much different than the sort that I make. That is a long story and today’s computers make vastly fewer errors.
Already in 1955 there was talk of computers checking or even finding mathematical proofs. It was mostly talk. Gelernter wrote a program that found a slightly shorter proof of one of Euclid’s early theorems. Today I do not expect to be entirely convinced by any computer checked proof of any program property that I really care about. I do hold out hope, however, that efforts toward computer checked proofs about certain classes of programs, will yield programs which are much more reliable.