Short: Generate Macro-assembler code from highlevel-language-like Commands
Formula generates Macro-assembler code from highlevel-language-like Commands,
which are enbedded in other Macro-assembler code (Code for the TLA macro-
assember).  For example, it can generate code for arithmetic expressions.