Thanks to Andrzej Trybulec, Czeslaw Bylinski, Grzegorz Bancerek and Roman Matuszewski for many interesting discussions and for looking after me during my visit to Bialystok, where this paper was started. For making this and other meetings of researchers possible, Bob Boyer deserves every credit; I am also grateful for his encouragement to write this paper. I have also benefited from conversations with Mike Gordon and with other people at the QED conference, and with members of the Programming Methodology group at Åbo Akademi. My visit to Poland was funded by the U.S. Office of Naval Research, and my later work was supported by the U.K. Physical Sciences and Engineering Research Council, the Isaac Newton Trust, and more recently by the European Commission under the Human Capital and Mobility programme. Piotr Rudnicki gave me some helpful comments on an early draft, and discussions with Randy Pollack about the issues of feasibility and extensibility were very stimulating.

John Harrison 96/2/22; HTML by 96/4/5