The questions "How does it work?" and "Why does it work?" have inspired everyone engaged in science or engineering research.

These days, their answers are incorporated into sophisticated computer programs: design tools that have contributed major advances in the quality, efficiency and reliability of the products of our technological society.

And this is often in ways that were inconceivable to those who engaged in the original research.

How do computer programs work? And why? Nobody really knows for certain. Or at least, nobody is certain enough to guarantee that they are going to work correctly.

Even what little we believe we understand may be inadequate, inappropriate, or even downright wrong.

Researchers in the science of programming have put forward a number of good theories. And in engineering practice there are many programs of all sizes in constant use that actually do their job pretty well.

In this, they are like those medieval cathedrals and bridges that amazingly still stand, although they were built long before our modern theories of civil engineering could explain how and why.

To build the link between the theory of programming and the products of software engineering practice is still a grand challenge for scientific research in computing.

The history of science records many examples where the pursuit of such a challenge has triggered a major scientific breakthrough.

A recent example is the Human Genome project. Projects such as this are long - 15 years in this case.

They have wide international participation, ideals of rapid and open publication, and a quest to answer basic questions that lie at the foundations of an entire scientific discipline.

Are there any projects in computer science that share these characteristics? A well-known computing grand challenge dating from the 1950s was the construction of a computer that played chess at international championship standard.

That challenge was met on 11 May 1997, when the IBM Deep Blue computer defeated the reigning world chess champion Garry Kasparov. Are there any more such challenges for computing research?

The verifying compiler is one. Its aim is the construction, evaluation and deployment of a high-level programming language compiler that verifies the correctness of each program it compiles.

If this project is successful, it could avert many of the programming errors that afflict the world today.

The verifying compiler will be built from a combination of the technologies already incorporated in software engineering tools, such as program analysers, code generators and development environments.

Its goal is to guarantee that every program it compiles will always work in the specified manner. For example, the compiled program will not hang, crash when mistreated, or succumb when attacked.

And under no circumstances will it ever crash the car or rocket it is helping to drive or fly.

The verifying compiler is a long-standing undertaking, but significant advances in hardware and software technology, and in the professional environment, offer new hope that the challenge could be met in the foreseeable future.

All the strands necessary for developing it are already here. We just need some way of weaving them together into a single program development and analysis tool, for use first by researchers, and later by professional programmers.

The announcement and planning of a grand challenge project is perhaps the only way of mobilising the available scientific talents and idealism to work co-operatively and competitively towards the answer to the basic scientific questions of software engineering and the theory of programming.

Professor Sir Tony Hoare is a senior researcher with Microsoft Research in Cambridge. This article is based on a lecture given at Gresham College in London last week.