Abstract:
The first part of the paper introduces the varieties of modern constructive
mathematics, concentrating on Bishop's constructive mathematics
(BISH). It gives a sketch of both Myhill's axiomatic system for BISH and
a constructive axiomatic development of the real line R. The second part
of the paper focusses on the relation between constructive mathematics
and programming, with emphasis on Martin-Löf's theory of types as a
formal system for BISH.