Syntax Definition Formalisms 3 (SDF3) is an academic syntax definition, used for compiling languages. It is part of the Spoofax workbench.
Syntax and language basics
Formal language definitions are very much related to (context-free) grammars, as we know them from automata.
Sorts are the categorization of both terminals and non-terminals. By defining something as a sort, we can use the declaration in something called productions. A grammar of a language consists of rules aka productions to build a valid program structure. A production consists of a sort, or sort constructor, followed by a body.
An example: `sorts Expr` `Expr = <Expr * Expr>`