Curry–Howard correspondence

The Curry–Howard correspondence is a deep and significant relationship between logic and computational theory, particularly between formal proofs in logic and programs in computer science. It fundamentally establishes a direct connection between: 1. **Logical Systems**: Types in programming languages correspond to propositions (statements that can be true or false) in logic. 2. **Programs**: Terms (or expressions) in programming languages correspond to proofs in logical systems.