A crucial tool is a rigorous analysis based on formal logic. The basic
ingredient is the ingredient of proof. And now I will give a brief history
of the notion of proof. Here I say western history of proofs, because
of course different tradition have dealt with the problem of formal mathematics
in different ways.
The origin of proofs in the western tradition comes with Plato, something
like 400 years BC, when in the so called "Meno's dialogue" Menos
is made to recall a proof of an instance of Pythagora's theorem.
Then Aristotele and Euclide later they were disciples of the Platonic
school - developed the notion of proof in logic and in mathematics.
But it was not until the twentieth century that the notion of proof -
which however had played the crucial role in mathematics and logic - became
an object of mathematical study itself. And this we owe essentially to
the work of Frege, Hilbert and Gentzen.
And it became a first class citizen with other mathematical objects only
with the intuitionistic school developed around the twenties by Brouwer,
Heyting and later expounded by Bishop in the so called constructive mathematics.
So you see it took nearly more than 2.500 years to actually start from
the acknowledgement of the importance of the notion of proof, to actually
consider it with other mathematical objects as a first class citizen.
Once this was achieved, it took only a few years to realise that formal
proof checking was indeed viable.
And finally we have in the seventies, with perhaps one of the most important
constructive mathematicians, the realisation that within proofs there
is a lot of computational contents, and this was the finally established
fact that proofs play indeed a very important role in computer science.
|
|