Temporal Logic

I was at Berkeley in 1954 when “temporal logic” was newish and hot in some sectors. It then meant an extension of sentential logic and there were many competing proposed axiom sets for variations of purpose. I sidestepped the whole field; to me goal was the immutable math whose sentential logic was dramatically simpler.

It seems temporal logic is back via trying to understand computers. It seems it has never disappeared. Perhaps it has found an important niche. I was already interested in computers in 1954 but I had no idea then that the semantics of a program would sometimes be so important; I made no connection.

This paper brought the (for me) fragmentary art back to me. Mark Miller brought it to my attention. An Older Talk. Corresponding old paper

The “Logic” in this “Temporal Logic” seems to come down via electrical engineering; yet relevant.

I cannot find a clear description of the semantics or axiomatics of any particular temporal logic. A model would help perhaps.

Rocks to stand on -- Projects

A machine whose semantics you can rely on. (fragment)

Faith that you can understand a very simple machine language program that you see in the machine’s memory. It reads correctness proofs in a simple yet concise format. The proof is about another program in memory to which the checker has read access.

Belief that correctness proofs about programs need not be more than several times the size of the program.

Isolation
This allows cohabitation of a computer with modules that you don’t trust or that you cannot afford to rely on.

I think it is easy to define conservatively “capability compliance” so that a simple compliance checker can check a program with no proof. Peter Deutsch did nearly this in 1968. This might aid kernel proofs.

Alternatively classic hardware protection mechanisms might be controlled by code whose logic must be correctness proven.

Yet alternatively some sort of capability hardware might suffice.