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.

everything hits the tokenizer at some point 💀 which is where all data meets their maker.

• a palm tree? 🌴 oh u mean generic tree with fancy leaves? 🌳❇️
• a chair? 🪑 oh u mean symbols arranged chair-wise?
• a heartfelt message to your crush? 💖 oh u mean char[]? (characters stringed together in a sequence)
• a wonderful picture? u mean a list of colors and a columns count?

everything loses detail after the tokenizer.