Constructive mathematics and computer science
Henry Cheng · 1972
This paper gives an informal exposition of the relationship between mathematics and computer science generated by the constructive viewpoint of Errett Bishop. Brouwer's insight on the lack of computational content in classical mathematics is discussed first. Then Bishop's constructivism is presented as a natural completion on the program started by Brouwer to develop a more realistic foundation for mathematics. Finally, the correlation between formal constructive mathematics and computer languages is illustrated and examined.