3 ms·
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
by 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 agoAlso, "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 agoOk, but students need to understand at least ¬, ∧, ∨, →, and there are other useful equivalencies as between sets and (characteristic) functions etc.