  In his Discourse on the Method of Rightly Conducting the Reason, and Seeking
Truth in the Sciences, Rene Descartes sought ``clear and certain knowledge of
all that is useful in life.'' Almost three centuries later, in ``The
foundations of mathematics,'' David Hilbert tried to ``recast mathematical
definitions and inferences in such a way that they are unshakable.'' Hilbert's
program relied explicitly on formal systems (equivalently, computational
systems) to provide certainty in mathematics. The concepts of computation and
formal system were not defined in his time, but Descartes' method may be
understood as seeking certainty in essentially the same way.
  In this article, I explain formal systems as concrete artifacts, and
investigate the way in which they provide a high level of certainty---arguably
the highest level achievable by rational discourse. The rich understanding of
formal systems achieved by mathematical logic and computer science in this
century illuminates the nature of programs, such as Descartes' and Hilbert's,
that seek certainty through rigorous analysis.
