So, you know how in programming you have data types (like int, float, structs etc…) well, they are actually math.
In math, more specifically in logics, there’s these things called “judgement derivation systems”. They are basically sets of rules that tells you if you can derive a judgement, from a set of hypothetical judgement. The most notorious are sequent calculus and natural deduction. Both are used to determine if a logic formula is consequence of a set of hypothesis.
You see, one day Mr Howard wrote to Mr Curry: “I was working on a type system for lambda calculus, and I noticed it kinda look like natural deduction” and curry answered: “wow, that’s cool, I’ll tell you more, a type system for this other thing kinda looks like combinatory logics” and then they both went “could it be that every type system is actually a logic deduction system, and every logic deduction system is actually a type system?” And this is what modern type theory (and theorem provers) are based on.
Now, formal type systems are often defined as judgement systems. More specifically, they look like sequent calculus, and they use a “context” object, which is often identified with the letter gamma.
I was aware of that, but I didn’t want to do a full write-up from zero knowledge to type theory…
Maybe I’ll do it later tho. Because I enjoy explaining this stuff.
Anyway, despite the comedic delivery, that comment should give a 1st year CS student all the keywords they need to research the subject. Especially the letters between Curry and Howard, which are referred to as the “Curry-Howard correspondence”
![type [...] rule??? (I legit dont know what this is)](https://leminal.space/pictrs/image/f764e024-3e48-4e9f-ba47-72f4e9259c83.png){kind=link}
Oooooohhh! That’s my field of study!
So, you know how in programming you have data types (like int, float, structs etc…) well, they are actually math.
In math, more specifically in logics, there’s these things called “judgement derivation systems”. They are basically sets of rules that tells you if you can derive a judgement, from a set of hypothetical judgement. The most notorious are sequent calculus and natural deduction. Both are used to determine if a logic formula is consequence of a set of hypothesis.
You see, one day Mr Howard wrote to Mr Curry: “I was working on a type system for lambda calculus, and I noticed it kinda look like natural deduction” and curry answered: “wow, that’s cool, I’ll tell you more, a type system for this other thing kinda looks like combinatory logics” and then they both went “could it be that every type system is actually a logic deduction system, and every logic deduction system is actually a type system?” And this is what modern type theory (and theorem provers) are based on.
Now, formal type systems are often defined as judgement systems. More specifically, they look like sequent calculus, and they use a “context” object, which is often identified with the letter gamma.
Not to be that person, but…
Don’t worry, it happens to the best of us.
Humour aside, I actually found it very interesting to read, despite not quite understanding it fully. I might give it a more thorough read later.
I was aware of that, but I didn’t want to do a full write-up from zero knowledge to type theory…
Maybe I’ll do it later tho. Because I enjoy explaining this stuff.
Anyway, despite the comedic delivery, that comment should give a 1st year CS student all the keywords they need to research the subject. Especially the letters between Curry and Howard, which are referred to as the “Curry-Howard correspondence”
I was joking, a bit. It’s not like you can explain all of it in one random comment.
Aghhh! I wanna get a cs degree, but I had to switch programs for r e a s o n s. Maybe I could get one after my associate’s degree.
I think they said programming was math
I’m really good at math