Imagine that a programming guru is asked by a person who wants to learn programming how to start. The guru tells the novice that he should get some nice Linux distribution like Gentoo that has all he needs – vi and gcc. He also shows the novice some Linux kernel code to demonstrate the wonderful things someone with knowledge of programming can do. The n00b is immediately enlightened. Or, more likely, runs away in horror.
Freek Wiedijk does something quite similar as this programming guru in his “Formal Proof – Getting Started“. He chooses two leading proof assistants – HOL Light and Mizar to demonstrate two proof styles – procedural and declarative. This may be considered a balanced view, but I think it is just a bad idea. HOL Light is a great system for use in industry – it is easier (reportedly, I have no personal experience) to write the proofs the procedural way. In industry the most important role of proofs is that they certify that an assertion is true. In mathematics proofs have also another role to fulfill: proofs convey knowledge. People study proofs not only to check if they don’t not contain mistakes, but also to find out why the assertion is true. Proofs written in procedural style do not provide this information, at least in an easily accessible way. Wiedijk provides a picture with a fragment of HOL Light formalization of the Law of Quadratic Reciprocity. This is enough to make most mathematicians reading the article hope that they retire before this style of mathematics becomes common.
The Mizar example is much better, but that in turn leaves the reader with the impression that this is the best the current tools have to offer. This is of course not true. First of all Wiedijk fails to mention that what is on those figures is the source, not the presentation. The distinction is obvious for mathematicians. Nobody shows people LaTeX source and suggests that this is how mathematical papers look like. Even Mizar can be presented in a much more readable way than its ASCII source. Of course a fragment of Isabelle/ZF proof document with a proof written in Isar would be the best (well, almost, a screenshot from the Tiddly Formal Math site would be the best).
When I was starting IsarMathLib it took me two months from downloading Isabelle to submitting a 0.0.1 version of IsarMathLib to Savannah with quite a lot of formalized general topology and group theory. That was possible because the foundation was familiar – I knew from school how mathematics is expressed in set theory. This made it a much easier task than if I had tried to do the same in HOL (actually, I did, and I gave up). Wiedijk does not mention a basic difference between HOL Light and Mizar – that one is founded on type theory and the other on set theory. While it is true that for most mathematicians the foundation does not matter, precisely those for whom it somewhat matters will be the first to try formalized mathematics. The readers of Wiedijk article may not know that in case of HOL Light they will not only have to learn the formal proof language, but also get used to a new understanding of the basic notions (like, say, that a function is not a set of pairs).
The Wedijk article contains some excellent pieces of formalized mathematics propaganda. The text on three main revolutions in “The Future of Formal Mathematic” was so familiar to my mind that it made me check if I hadn’t written something like that on this blog (I didn’t, must have seen this in some earlier Wedijk article). Wedijk finishes
People who do not like programming or who do not like mathematics probably will not like formalization. However, for people who like both, formalization is the best thing there is.