Are these two sensible and related or unrelated ways of regarding a logic system as a programming language?
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.