I was just reading Per Martin-Löf's On the Meanings of the Logical Constants and the Justifications of the Logical Laws [0] which talks about this exact notion

I was just reading Per Martin-Löf's On the Meanings of the Logical Constants and the Justifications of the Logical Laws [0] which talks about this exact notion from Martin-Löf's modern intuitionistic logical perspective. This paper is a little dense and meandering, but I challenge anyone with an interest in the relation of programming and mathematics to take it on. An ultimate conclusion it attempts to justify is that theory and proof (identical to "type and program") are a noun and a verb respectively. The act of consuming a proof is the one where you, the reader, consume some evidence which subsequently substantiates the proposition of interest. What that means in relation to this parent's notion is that mathematics, and indeed programming or anything which can be connected so strongly to formal logic, necessarily draws all of its meaning from the words used to express it... and thus, once you've heard them (read a proof, seen a program) you have all of the facilities necessary to manipulate it and test it and learn more. Which is exactly what makes all of these bodies of work, together, so accessible and wonderful. And it's exactly why history always feels less powerful. [0] http://www.ae-info.org/attach/User/Martin-L%C3%B6f_Per/OtherInformation/article.pdf http://www.ae-info.org/attach/User/Martin-L%C3%B6f_Per/Other...