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.
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.
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.
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.