Are these two sensible and related or unrelated ways of regarding a logic system as a programming language? When I am trying to understand logic programming languages e.g. Prolog, I am immediately confused by the following two ways of relating logic systems and programming languages or type systems.


In Types and Programming Languages by Pierce, Section 9.4
Curry–Howard correspondence on p109  has a table



Does it mean that a logic system is a programming language, where


types are propositions and
values of a type are proofs of the proposition?

On the other hand, a logic system is described in a formal language
that defines what a logic expression is. Can we view a logic system
(e.g. the first order predicate logic system) as a programming
language, where


it has two types: Boolean type and function type, and 
Each logic expression without a variable has Boolean type, so can be evaluated to a truth value.  Each logic expression with any
variable has Boolean function type, so its application to truth
values for its variables can be evaluated to a truth value?



Are the above two views of a logic system as a programming language completely unrelated/orthogonal, or are they the same or can they be unified?

Thanks.
Does it mean that a logic system is a programming language, where types are propositions and values of a type are proofs of the proposition?


Not necessarily, being both (logic systems and programming language) formal languages, there certainly is a certain degree of isomorphism between the two concepts, this translates into the fact that we can encode a logical system through a programming language and develop algorithms to identify proofs of the theorems of our logical system. 

If you are interested in the similarities between logical propositions and types, I strongly suggest you take a look at Homotopy type theory.