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.
Comments
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.
That only exists in theoretical computer science. In real computer programming, you always have some bounds to the value of A.
I think it is time to repost Against Curry-Howard Mysticism (https://liamoc.net/forest/loc-000S/index.xml)