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 th…
> many ideas are more accessible to me in type theory as opposed to logic But how do you understand type theory without some basic understanding of logic?
It's possible, but I guess I should have specified "logic outside the standard curriculum of computer science studies." For example, I think understanding bits of modal logic through how monads behave is much more fruitful for a CS person. Also, I want to further add here that the correspondence between proofs and programs is known as the Curry–Howard correspondence. This is the more general term under which these relationships between type theory and logic are discussed. The term "computational trinitarianism" also adds a further correspondence to categories. ( As shown in my link above ).