Abstract
Gilles Dowek, professor at the École Polytechnique, is the author of the book "Les métamorphoses du calcul" (The Metamorphoses of Calculation), which won the Grand Prix de philosophie de l'Académie Française in 2007. He discusses the relationship between computation and proof, obviously central to program verification. He showed that algorithms historically preceded demonstrations, as proven by numerous clay tablets of various origins, and that these algorithms were probably proved correct in unwritten ways. The notion of formal demonstration was introduced later by the Greeks, probably on the basis of algorithms already in existence or invented to solve specific problems, before being developed for its own sake and founding mathematics. Well-known theorems such as Thales and Pythagoras actually correspond to algorithmic problems. An analysis of Euclid's proof of the algorithm for calculating gcd by subtraction shows its very close relationship with modern methods of proving programs, which are of course concerned with much larger objects, with correlatively much larger demonstrations that need to be verified themselves by computer.
