What are Formal Methods?

Formal methods may be defined as a branch of discrete mathematics which deals with the logical analysis of forms and their semantics (meaning), with a specific application domain being computing. They usually consist of two parts:

1. a formal calculus (or formal system) which is a symbolic system in which are defined axioms, having some denotation as formulae; a precise syntax that defines how the axioms may be put together; and relations that enable the deduction of properties purely as the conclusion of arguments that are valid through the system's syntax.
2. a formal language is a formal calculus which has also an interpretation of the formulae -- semantics. Further rules constrain what constitute valid (meaningful) formulae and the properties that may be deduced. A given calculus may have infinitely many interpretations.

At first sight this may appear off-putting to an engineer who is unfamiliar with this kind of maths. It is rather a contrast with the usual conotation of 'methods' in industry, which are procedures to generate working products. As many authors have pointed out, the general lack of such an industrial view, has proved a great stumbling block.

However, the second part allows the more liberal view that formal methods may be regarded as a mathematical approach to {reason about} any system, be it an industrial factory or an abstract machine. It is just another language to make ourselves clearly understood by others and continue development in a sure-footed manner. Further, there are efforts to integrate the formal approach into working methodologies that are recognised by industry.