If you take a class in compilers you should see these sorts of inference rules when talking about operational semantics. Though maybe it isn't as popular to use operational semantics anymore. It's very useful to define rules in this syntax when working on semantic analysis and code generation.

I didn't get the background really necessary to really understand the type-theory parts of this notation until I took a graduate course in programming language theory.