Usually, they take the form of logical implications written in a Metalanguages.
When you implement a compiler, the meta-language will be the language you use to implement the compiler. However, it's quite common for researchers and designers to describe type systems using English, or formal logic (also sometimes called math).
In this course, we will often use inference rules to describe type systems.
What an inference rules describes is an implication between premises and a conclusion. We write the premises above a line, and the conclusion below the line.
What an inference rule means is this: if the premises are true, then the conclusion is true.
There are several things that make typing rules tricky.
First, as we said, they are specified in a Metalanguage, which talks about an object language. One source of confusion is to get confused about which language an expression is part of.
For example, if we write the following typing rule for addition:
You may ask yourself the following questions:
The second thing that makes inference rules tricky to understand is that often, program analysts want to work backwards. We want to check if the conclusion could be satisfied (for instance, in type inference), and therefore we need to check if the premises could be satisfied as well.