John Harrison.
Notices of the American Mathematical Society, vol. 55, pp. 1395-1406, 2008.
Abstract:
A formal proof is a proof written in a precise artificial language that
admits only a fixed repertoire of stylized steps. This formal language is
usually designed so that there is a purely mechanical process by which the
correctness of a proof in the language can be verified. Nowadays, there are
numerous computer programs known as proof assistants that can check, or even
partially construct, formal proofs written in their preferred proof language.
These can be considered as practical, computer-based realizations of the
traditional systems of formal symbolic logic and set theory proposed as
foundations for mathematics.
Bibtex entry:
@ARTICLE{harrison-notices,
author = "John Harrison",
title = "Formal Proof -- Theory and Practice",
journal = "Notices of the American Mathematical Society",
volume = 55,
year = 2008,
pages = "1395--1406"}