The Curry-Howard correspondence. For instance, in mathematics, we have A ⇒ A (every statement implies itself, for instance "if it rains, then it rains"); and a

The Curry-Howard correspondence. For instance, in mathematics, we have A ⇒ A (every statement implies itself, for instance "if it rains, then it rains"); and analogously, in programming, we have the identity function of type A → A (which reads a value as input and outputs the same value). This is the tip of an enormous iceberg identifying, in a certain precise sense, proving with programming (and stating mathematical assertions with specifying the desired behavior of a program). However, programming is a bit more general than proving: Circular proofs are simply of no value, whereas looping programs can still be valuable. For instance, I for sure hope that the main loop of the browser I'm currently using to fill out this textbox does not prematurely stop.