Formal system
In mathematics, a formal language is usually not described by a formal grammar but by (a) natural language, such as English. Logical systems are defined by both a deductive system and natural language. Deductive systems in turn are only defined by natural language (see below).
The QED manifesto represented a subsequent, as yet unsuccessful, effort at formalization of known mathematics.