Fyi, there are many correspondences between logic and type theory / functional programming. I have found that as a programmer, many ideas are more accessible to me in type theory as opposed to logic. Languages like Haskell are great for exploring these relationships.
This is also known as computational trinitarianism - https://ncatlab.org/nlab/show/computational+trinitarianism
Robert Harper, the computer scientist that coined "computational trinitarianism," has a series of lectures on the foundations of type theory including some commentary on these correspondences - https://youtu.be/9SnefrwBIDc.