3 ms·

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

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 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 https://youtu.be/9SnefrwBIDc.

_emacsomancer_ 8y ago
> 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?
- BucketSort 8y ago
  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 ).
  - BucketSort 8y ago
    Also, "Curry–Howard–Lambek correspondence" is the real name for "computational trinitarianism." I like the latter better because I don't like naming mathematical things after people, which have no bearing on the actual meaning.
  - _emacsomancer_ 8y ago
    Ok, but students need to understand at least ¬, ∧, ∨, →, and there are other useful equivalencies as between sets and (characteristic) functions etc.
- trentmb 8y ago
  They probably don't- its similar to how everyone that plays poker is somehow an expert at game theory.

_emacsomancer_ 8y ago

> 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?

BucketSort 8y ago
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 ).
- BucketSort 8y ago
  Also, "Curry–Howard–Lambek correspondence" is the real name for "computational trinitarianism." I like the latter better because I don't like naming mathematical things after people, which have no bearing on the actual meaning.
- _emacsomancer_ 8y ago
  Ok, but students need to understand at least ¬, ∧, ∨, →, and there are other useful equivalencies as between sets and (characteristic) functions etc.
trentmb 8y ago
They probably don't- its similar to how everyone that plays poker is somehow an expert at game theory.