 The systematic explanation and formalization of intuitionistic logic was begun by Brouwer’s student Arend Heyting in 1928. An “explanation” here is an account of what one knows when one understands and correctly uses the logical connectives. Since the 1970s Heyting’s explanation and its variants are known as “the Proof Interpretation”, as the role played by mind-independent truth in explanations of classical logic is here played by proof. For Heyting, a proof was primarily a mathematical construction in Brouwer’s sense, and, secondarily, a linguistic description of it. But it turned out that a Proof Interpretation can also be based on other notions of proof. The Proof Interpretation understood in a more general sense has found many applications outside its historical origin, notably in other constructive but non-intuitionistic forms of mathematics, philosophy, computer science, and linguistics. This widening of the range of application was possible because the original Proof Interpretation depends mostly on the fact that the intuitionistic notion of mathematical truth is of a verificationist nature, so that broadly verificationist theories in other domains allow for an analogous explanation of their logic.