##
**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.

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

### MSC:

03F55 | Intuitionistic mathematics |

03F50 | Metamathematics of constructive systems |

68Q65 | Abstract data types; algebraic specification |

68N01 | General topics in the theory of software |