For example, in some colleges the procedures taken against failing students have been set out as a formal system. This gives greater clarity, of course accompanied with a loss of flexibility. Procedures for immigration and naturalisation have tended over time towards more formal models.
In mathematics, formal proofs are the product of formal systems, consisting of axioms and rules of deduction. Theorems are then recognised as the possible 'last lines' of formal proofs. The point of view that this picture encompasses mathematics has been called formalist. The term has been used pejoratively. On the other hand, David Hilbert founded metamathematics as a discipline designed for discussing formal systems; it is not assumed that the metalanguage in which proofs are studied is itself less informal than the usual habits of mathematicians suggest. To contrast with the metalanguage, the formal grammar itself is often called an object language (i.e., the object of discussion - this distinction may have been introduced by Carnap). The object language/metalanguage distinction used in computer science is a little different.
It has become common to speak of a formalism, more-or-less synonymously with a formal system within standard mathematics invented for a particular purpose. This may not be much more than a notation, such as Dirac's bra-ket notation.
See also mathematical logic.
