Apple iPhone users are greeted with a silent alarm at the first day of 2011 (see here and here). All evidence points to a software bug in the operating system.

This is not the first widespread software bug from a well-known manufacturer. In 1994, a math professor found that the Intel Pentium CPU had a bug when doing divisions. It caused a sensation in the IT world (see here), and ultimately Intel recalled all flawed processors.

All modern electronic devices (your desktop, laptop, notebook, netbook, digital camera, mobile phone, mp3 player, etc.) contain software. These software are designed and implemented by smart engineers, and checked and tested by a team of testers. The aim is to get rid of every last software bug. After all these rigorous processes the software is 99.99999% correct — but it is the 0.00001% that embarrasses the company.

The only way to claim the perfect 100% is to prove it, mathematically. This means translating the design and implementation into the language of math, and to show that the implementation follows logically from the design. This is tedious work, not usually done by a human mathematician. Rather it is the job for theorem-provers, special programs that can perform automated reasoning.

You’ve probably never heard of these terms. It’s because traditionally theorem-provers exist only in universities, for academics doing research in automated theorem proving. Since the Pentium bug, hardware companies (like AMD) are relying on theorem-provers to verify microprocessor designs. Even software companies (like Microsoft) are doing research in theorem proving.

Now if you put on your logic hat, you’ll find an interesting situation: theorem-provers are themselves software coded by human, how can we be sure that theorem-provers don’t have bugs?

The answer is: we can’t be sure, but we do take measures to reduce the chance of any bugs.

Firstly, theorem-provers have a very small core, call the inference engine. Basically, it is capable of manipulating symbols, according to a few simple rules. Keeping everything simple means less hiding spots for bugs. The system starts with a few fundamental math facts (like every number has a next one), and requires any additional facts must be first proved by the inference engine. Thus the system builds up its power on a firm basis.

Secondly, theorem-provers are open-source projects. This means the source code of system, in particular its core inference engine, is open for inspection. In these days of Internet, you can download the source code. With appropriate tools, you can compile the codes and run the system in your own computer. People with like interest in the system will form a group checking the merits of the system, and contribute to any bug-fix or improvement of the source code. There is a saying in IT community: *“given enough eyeballs, all bugs are shallow”*.

The theorem-prover I’m using for my project is HOL4, which is open-source with a small core. Here is a readable introduction, and here is a technical overview.

My supervisor is one of the main developers of HOL4.

## Leave a Reply