History for Message from Tony Hoare

added:
 

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.