The subject of formalized mathematics has shown up in Slashdot discussions a couple of times. Every time that happened someone mentioned Gödel inconsistence theorems and from that point on much of the discussion concentrated on how Gödel results imply (or not) that formalized mathematics is impossible, impractical or useless.
When I see a discussion like this I think how some seventy years ago a similar forum would discuss the idea that it would be possible and useful to do away with human computers and use machines to execute algorithms. There would be similar arguments about how you could not do that because to execute an algorithm one has to understand it first and machines can not uderstand anything. The art of designing algorithms would lose its beauty when the algorithms would have to be written in a machine language. And, due to a deep theoretical result called the “halting problem” we would have no way to know in advance if such algorithm would ever stop to produce a useful result.
It is easy to dismiss Slasdot discussions and blame them on the general cluessness of the Slashdot crowd. However, I recently stumbled upon the text of a talk given by Chaitin at the University of Cordoba in November last year that completely puzzled me.
It has all the typical elements – a story of Hilbert’s dream to “formalize mathematics completely in such a way that there is an algorithm, a mechanical procedure, for checking whether or not a proof is correct” an how “Kurt Gödel showed that Hilbert’s project could never work”.
Chaitin knows what Gödel incompleteness theorems are about and is not afraid of computers, so I don’t understand why is he so confused about formalized mathematics. Some of the things he writes are really bizarre, like
Furthermore, they envision an official repository for formal proofs that have been put through this verification process. Proofs will have to be accepted by this repository to be used by the mathematics community; everything that has been formalized and checked will be there, in one place.
Sounds almost like a warning about a plot to create a world government.
Most annoying to me is his conviction that formalized math is somehow in opposition to creativity. He asks “is mathematics creative or is it mechanical?”. Well to me the answer is simple: creating a proof is creative, checking it is mechanical.
The process of creating formalized mathematics is similar to programming in that it consists of two phases: coming up with an idea for the proof (kind of like design in programming) and putting it in formalized form (implementation). In romantic math one stops at the first phase. I am sure that there are software designers who are unable to code, but I think being able to implement the design makes a better designer, not a less creative one. Similarly, I believe being able to write proofs in a formal language makes one a better mathematician.
Ok, I am done with Chaitin. On an unrelated subject, there is an interesting discussion on the Lambda the Ultimate blog/forum about similarities and differences between COQ and Isabelle. I especially like the following opinion by Steven Obua:
If you are proving a program to be correct, you actually don’t need your program to have an advanced type system at all (again: simple types are useful just for not needing to deal with raw sets), because you can express everything you want to say about this program in normal mathematical theorems.
This is what I think too. I prefer to program in statically typed languages. A good type system is a very useful and cheap substitution for formal verification. But if you could have the real thing (without types) there would be no need for types.