The Notices of the American Mathematical Society has published a special issue on “formal proof”, leading off with an article [pdf] on the where the field stands. I find this subject exciting because of its promise, not just as a tool in mathematics, but to solidify the foundations of the computational world.
A formal proof is a mathematical proof of a special kind: one presented in a notation and level of detail that can be checked for correctness by relatively simple, deterministic computer algorithms. “Formal” here means that the proof makes no appeal to understanding, but relies only on rules for symbol manipulation to derive theorems from axioms. Today, formal proofs are developed by painstaking formalization of conventional proofs, at a rate of about one week of mathematical labor per page of journal text. The result is mind-numbingly detailed, and is longer than the human text by a surprisingly consistent ratio called the de Bruijn factor (about 4). A grand objective of the field is to formalize the whole of mathematics, (re-)proving its theorems with a negligible probability of error, all based on a small kernel (in the HOL Light system, the kernel is about 500 lines of OCaml code).
Why does this matter to us ordinary mortals? Because proof methods can be applied to digital systems, and in particular, will be able to verify the correctness (with respect to a formal specification) of compilers [pdf], microprocessor designs [pdf] (at the digital-abstraction level), and operating system microkernels (the link points to a very important work in progress). Software tools for computer-assisted proof are becoming more usable and powerful, and they already have important industrial-strength applications [pdf]. In a world which increasingly relies on computers for everything from medical devices to national governance, it will be be important to get these foundations right, and to do so in a way that we can trust. If this doesn’t seem important, it may be because we’re so accustomed to living with systems that have built on foundations made of mud, and thinking about a future likewise based on mud. All of us have difficulty imagining what could be developed in a world where computers didn’t crash, were guaranteed to be immune from virus attack, and could safely download code written by the devil himself, and where crucial pieces of software could be guaranteed to not leak data.
In this area, as everywhere in the realm of fundamental technological progress, the possibilities we can imagine will become the basis for possibilities we can’t imagine, and these, as they become real, will make possible yet more. We started with stone tools, and look where that led. Closer to our home in history, consider the consequences of personal computer networks and internet-based hypertext publishing. Looking forward from the 1980s, some of us were excited by the prospects (here’s a paper I wrote), but no one could foresee more than the outlines of a small part of what has emerged.
And some of what we’d hoped for from (what is now called) the Web hasn’t happened because the foundations of computation are still mud, and no one yet dares try to build very high.
{ 4 trackbacks }
Comments on this entry are closed.