logic of the month club You make it sound as if theorists were inventing logics frivolously. We have known since the stone age (of computing) that we can reas

logic of the month club You make it sound as if theorists were inventing logics frivolously. We have known since the stone age (of computing) that we can reason about any computation using e.g. ZFC set theory, since we can formalise the operational semantics of any computation in ZFC. The problem is that general purpose logics like ZFC are extremely inefficient (in the sense of having too large a proof search space). For example ZFC allows you to reason about statements like: 4 \in squareroot(3). But such questions are meaningless in reasoning about programs. ZFC is too expressive. What all the work on program logics is about is to find logics that are 'more efficient'. That means they should be (1) Expressive enough to enable reasoning about program propertise that we care about. (2) Make the proof search space as small as possible. (3) Make specification and reasoning convenient (for computer or programmer). All the logics you mention make some progress towards these goals. Nominal logic for example makes reasoning about programs with binders more efficient. Separation logic makes reasoning about stateful computation more efficient. Type theories are progress towards integrating programming, specification and proving (whether that's desirable or not is a contentious question). The LCF approach gave use the currently dominant interactive theorem prover architecture. Linear logic has been the single most influential idea in the last 3 decades in the design of typing systems, especially for concurrent systems. write more assertions Should they be checked statically or dynamically?