Constructive mathematics and computer programming. (English) Zbl 0541.03034

Logic, methodology and philosophy of science VI, Proc. 6th int. Congr., Hannover 1979, Stud. Logic Found. Math. 104, 153-175 (1982).
[For the entire collection see Zbl 0489.00005.]
It is common knowledge that there are close relations between constructive mathematics and computer programming (as a disciplin). This article explains with great clarity the most important aspects of these relations. For constructive mathematics the author takes his system of intuitionistic type theory. In the programming area concepts introduced by Dijkstra, Hoare and Wirth are discussed. The reviewer found also the concluding remarks about Automath quite interesting. He would like to add that it would be a fruitful research object to exploit the relations to the ”computational logic” developed by Boyer and Moore.
Reviewer: M.M.Richter


03F55 Intuitionistic mathematics
03F50 Metamathematics of constructive systems
68Q65 Abstract data types; algebraic specification
68N01 General topics in the theory of software


Zbl 0489.00005