The Curry-Howard correspondence is a profound discovery that links computer science and mathematical logic. It establishes a connection between mathematical proofs and computer programs, elevating programming to the level of mathematics. The correspondence was independently discovered by Haskell Curry and William Alvin Howard, who noticed the similarity between functions in mathematics and the implication relationship in logic. This correspondence has practical applications in both computer science and mathematics, such as software verification and the development of proof assistants. Researchers are still exploring the implications of this link between math and programming and discovering more instances where different logical systems correspond to computational systems.
https://www.quantamagazine.org/the-deep-link-equating-math-proofs-and-computer-programs-20231011/