This is an essay about how I came to think that formal logic technologies can be useful in mathematics and computer science. It is shaped as a tree for I have not yet found a simple and logical ordering of the contents.

I examine and explain some of my beliefs about formal logic systems. First here is how and some of what I learned about them. I highly recommend this book which is largely about why and how others care.

In summary however, I have become convinced that:

The statements of formal systems that I dealt with were all short and certainly finite. The programs whose correctness I worry about all not only terminate but in times that I can afford to wait for. They run in a finite amount of memory using finite integers. I very seldom attempt to prove things about floating point as the semantics are obscure. (exception) The programs whose correctness I care most about use non-negative integers less than 264.

I suspect that I do not need a system that has a name for the set of integers, but perhaps I am wrong here.

I think that any proof that I need to verify is a sequence of fairly short propositions, but perhaps a very long sequence.

Of course I agree with the widely quoted caveat that the problem with formal proofs is understanding what you have proven.

A course by Benson Mates
Category digression