Experience using type theory as a foundation for computer science

Type theory is an elegant organisation of the fundamental principles of a foundational theory of computing, with theory taken in the sense of a scientific theory as well as a deductive theory. This theory generates a research programme. I examine the elements of this programme and assess progress. A large number of people world wide have been pursuing the type theory aspects of this research programme, so we can survey a large body of work created over a 20 year period for hints of success and failure and challenge. I first look at a few successes. Some of the applications we have attempted have not worked out as expected, and we don´t know whether the fault lies with the type theory or elsewhere. I first describe a failure that is clearly not the type theory, but the state of the foundations of computational mathematics. Then we look at problems closer to the structure of modern type theories-problems suggested by the success of classical set theory