  At a given moment these two senses met. H. B. Curry and W. Howard realized that the set of implication-only intuitionistic deductions was a core functional language called simply-typed \(\lambda\)-calculus: the programming language was a logic, the logic a programming language. This memorable meeting was called the ‘Curry-Howard isomorphism’  (Howard 1980).