Formal linguistics is the branch of linguistics which uses applied mathematical methods for the analysis of natural languages. Such methods include formal languages, formal grammars and first-order logical expressions. Formal linguistics also forms the basis of computational linguistics. Since the 1980s, the term is often used to refer to Chomskyan linguistics. 
Methods of formal linguistics were introduced by semioticians such as Charles Peirce and Louis Hjelmslev. Building on the work of David Hilbert and Rudolf Carnap, Hjelmslev proposed the use of formal grammars to analyse, generate and explain language in his 1943 book Prolegomena to a Theory of Language. In this view, language is regarded as arising from a mathematical relationship between meaning and form.
The formal description of language was further developed by linguists including J. R. Firth and Simon Dik, giving rise to modern grammatical frameworks such as systemic functional linguistics and functional discourse grammar. Computational methods have been developed by the framework functional generative description among others.
Dependency grammar, created by French structuralist Lucien Tesnière, has been used widely in natural language processing.
Analytical models based on semantics and discourse pragmatics were rejected by the Bloomfieldian school of linguistics whose derivatives place the object into the verb phrase, following from Wilhelm Wundts Völkerpsychologie. Formalisms based on this convention were constructed in the 1950s by Zellig Harris and Charles Hockett. These gave rise to modern generative grammar. It has been suggested that dependency relations are caused by a random mutation in the human genome.
Generative models of formal linguistics, such as HPSG, have also been used in natural language processing.