> a full system for [knowably-non-buggy] programming will be at the same time a full system that will suffice for the description of constructive mathematics.

> a full system for [knowably-non-buggy] programming will be at the same time a full system that will suffice for the description of constructive mathematics. That's basically the Curry-Howard correspondence[0], which was first explicitly stated in 1980. 0: https://en.wikipedia.org/wiki/Curry-Howard_correspondence https://en.wikipedia.org/wiki/Curry-Howard_correspondence