Message from Tony Hoare

Please convey to all the participants my greetings and best wishes in your deliberations. I will be with you in spirit, though I cannot attend in person.

I am looking forward to your initial answer to the basic question which I asked in Zurich: would it contribute to scientific progress in our field if our scientific community rallied behind some such slogan as

A million lines of automatically verified code?

This is a genuine question: and a considered negative answer is a realistic and acceptable reply. But a positive response could provide motivation and structure for the answers to all the other questions that you will be addressing before you can embark on such a major collaborative project. Here are some example questions.

How will we obtain agreement on the initial content of the million lines of challenge code? In what languages? In what application areas? Perhaps we should leave the final decisions until later, and consult outside interests in selection between programs of equal scientific interest.

How do we attract scientists to do the hard work of annotation and proof? Better tools are surely part of the answer. The tool-builders should discuss their personal plans for making their existing tools more attractive and efficient in use (very necessary, since a million is a big number). How can we take more effective advantage of feed-back from users in the evolution of tools?

Is their any advantage in assembling larger teams to build more comprehensive tools, perhaps exploiting agreed internal interfaces? For example, should the next generation of theorem provers continue with the Simplify interface, because that is the one that is currently in widest use?

Of course there are many more important questions which I am not even competent to ask. Just one word of advice: if the question has the form: Shall we do this or that? the answer should nearly always be Both!. Set up an experiment and decide the issues later.

And answering questions is not the most important thing. It would be a very happy outcome of the meeting if it just encouraged two or more of the participants to realise that they could achieve more ambitious scientific goals more quickly by working in collaboration or in scientific competition; and that they resolve in fact to do so immediately after they leave.