Excellent! Your answers are right, and you even correctly named the programming technique that corresponds to syllogism. Thanks again for participating.
when you think about it some more you start to wonder "what can be more proof than existence?"
This is a great point, and leads into one of the key differences between the logic of the C-H correspondence (called constructive or intuitionistic logic) vs. classical logic. Here's something to think about: In classical logic, we accept that either A or ¬A must be true (law of excluded middle). There's no way to prove that using types, so the C-H correspondence just rejects it! Constructive logic is a more limited, skeptical form of logic than classical logic.
I'd love to write about theorem provers and dependent types at some point, but honestly a lot of it is still over my head. :) I might have to build up to it. In the meantime, if you find this topic interesting, I encourage you to:
Look into functional programming languages (such as F#), where the C-H correspondence is much easier to see. I had fun writing these examples in C#, but the core ideas really belong to the functional programming world.
Think about what Tuple<A, B> corresponds to in logic. Then take a look at the Either<A, B> type (link) and think about what it corresponds to.
Bonus: There's actually a totally different correspondence between types and algebraic operations (e.g. addition, multiplication, exponentiation) that will blow your mind yet again, called algebraic data types. I might try to whip up an article or two on that concept as well.
Thanks, Brian. That was a really interesting challenge, both for the code and also to make me think differently about the meaning of the code.
I've never come across constructive logic before. It feels more natural, more "real world" than the usual binary logic. It also feels close to the statement "the world is all that is the case" in the sense that if we cannot construct it (that is, instantiate it) then in it should not be discussed! All that leading to recognising that statements like "if a tree falls in a forest, does it make a sound?" are not actually real questions.
Having a maths (translation: math! :) ) background, I'm interested in correspondences between maths and programming. So, being also interested in FP I end up reading about Category Theory quite often. There is some work going on (totally inaccessible for all but the best mathematical minds, which is a very, very long way from me!) that is looking at making a change to something that is fundamental in maths - equality. The redefinition of logic you mention seems to be a similar fundamental shift in thinking.
Thanks also for the pointers and links. I'll follow those up. Apart from the F# link, that is, as I am happy to say that I spend half of my time writing F# :) (which is how I came across your articles).
I'll look forward to reading some more from you in the future! :)
Category theory is a fascinating topic. Will read the article. Thanks.
If you find constructive logic interesting, you might also want to look into type theory, which uses constructive logic to replace set theory as the foundation for all math(s).
For further actions, you may consider blocking this person and/or reporting abuse
We're a place where coders share, stay up-to-date and grow their careers.
Excellent! Your answers are right, and you even correctly named the programming technique that corresponds to syllogism. Thanks again for participating.
This is a great point, and leads into one of the key differences between the logic of the C-H correspondence (called constructive or intuitionistic logic) vs. classical logic. Here's something to think about: In classical logic, we accept that either
Aor¬Amust be true (law of excluded middle). There's no way to prove that using types, so the C-H correspondence just rejects it! Constructive logic is a more limited, skeptical form of logic than classical logic.I'd love to write about theorem provers and dependent types at some point, but honestly a lot of it is still over my head. :) I might have to build up to it. In the meantime, if you find this topic interesting, I encourage you to:
Look into functional programming languages (such as F#), where the C-H correspondence is much easier to see. I had fun writing these examples in C#, but the core ideas really belong to the functional programming world.
Think about what
Tuple<A, B>corresponds to in logic. Then take a look at theEither<A, B>type (link) and think about what it corresponds to.Bonus: There's actually a totally different correspondence between types and algebraic operations (e.g. addition, multiplication, exponentiation) that will blow your mind yet again, called algebraic data types. I might try to whip up an article or two on that concept as well.
Thanks, Brian. That was a really interesting challenge, both for the code and also to make me think differently about the meaning of the code.
I've never come across constructive logic before. It feels more natural, more "real world" than the usual binary logic. It also feels close to the statement "the world is all that is the case" in the sense that if we cannot construct it (that is, instantiate it) then in it should not be discussed! All that leading to recognising that statements like "if a tree falls in a forest, does it make a sound?" are not actually real questions.
Having a maths (translation: math! :) ) background, I'm interested in correspondences between maths and programming. So, being also interested in FP I end up reading about Category Theory quite often. There is some work going on (totally inaccessible for all but the best mathematical minds, which is a very, very long way from me!) that is looking at making a change to something that is fundamental in maths - equality. The redefinition of logic you mention seems to be a similar fundamental shift in thinking.
Thanks also for the pointers and links. I'll follow those up. Apart from the F# link, that is, as I am happy to say that I spend half of my time writing F# :) (which is how I came across your articles).
I'll look forward to reading some more from you in the future! :)
Category theory is a fascinating topic. Will read the article. Thanks.
If you find constructive logic interesting, you might also want to look into type theory, which uses constructive logic to replace set theory as the foundation for all math(s).