Is there a relationship between "sound and complete" in logic and "type safety" in PLs?

I've been wondering if there's a connection between "good logics" and "good programming languages". It seems that logics are shown to be "locally sound and complete" whereas programming languages are shown to be "type safe" (preservation and progress).

If there's a relationship could you please explain it and give some references so that I can follow up on it.

Soundness and completeness of logic are semantic notions which say that logic and its models fit together nicely. We can find similar theorems in the theory of programming languages but they are not necessarily about mathematical models of programming languages.

A general way to understand soundness is that "bad things do not happen" (logic does not prove invalid things). A general way to understand completeness is that "good things happen" (there are sufficiently many models).

A programming language typically has several kinds of semantics:

• static semantics explains how to assign types to programs

• dynamics (operational) semantics explains how to run programs, more or less

• denotational semantics is more akin to models in logic and it explains how to map programs to mathematical objects.

There are theorems which relate these semantics. For instance:

Preservation: If a program p has type T and p evaluates to p' then p' has type T.

This is like soundness (bad things don't happen, namely a program will not become untyped). Another one is:

Progress: If a program p has type T then it is either a value (it's finished) or it has another step of execution.

This is like completeness (good things happen, namely a program will make the next step).

When we put these two together, we get safety.

Another kind of theorems relates denotational semantics to operational semantics. For instance:

Adequacy: if p and q are denoted by the same mathematical object then they are observationally equivalent.

Full abstraction: if p and q are observationally equivalent then they are denoted by the same mathematical object.

Adequacy says that the model is not too small and full abstraction that it is not too big. It makes a bit less sense to relate these two to soundness and completeness, but if I had to, I would say that full abstraction is like soundness and adequacy is like completeness.

StackExchange Computer Science Q#58110, answer score: 7