An interesting published review of this relationship is "Physics, Topology, Logic and Computation: A Rosetta Stone", by John C. Baez, Mike Stay <a href="https://arxiv.org/abs/0903.0340" rel="nofollow">https://arxiv.org/abs/0903.0340</a>. The first author alos has lots of interesting stuff related to (quantum) computation on his website.
This link surfaced on HN before. :)<p>505 days ago to be precise during a discussion of the article “Relation Between Type Theory, Category Theory and Logic” on <a href="https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory" rel="nofollow">https://ncatlab.org/nlab/show/relation+between+type+theory+a...</a><p>Fascinating topic, previous discussion: <a href="https://news.ycombinator.com/item?id=9867465" rel="nofollow">https://news.ycombinator.com/item?id=9867465</a>
> Imagine a world in which logic, programming, and mathematics are unified, in which every proof corresponds to a program, every program to a mapping, every mapping to a proof!<p>For those of you that may not know, this is called the Curry-Howard(-Lambek) Correspondence[1]. It establishes an isomorphism between well-formed computer programs and formal logic. This isomorphism is fairly intuitive when doing something like (typed) λ-calculus, but it also applies to things like Java and C++.<p>[1] <a href="https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence" rel="nofollow">https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...</a>
Unfortunately the most beautiful form of that analogy is the one that's crippled on both sides: computation (without Turing completeness) is equivalent to logic (without excluded middle). Add Turing completeness and you lose soundness. Add excluded middle and you lose confluence. Of course you can put epicycles on top of the simple idea and make it do anything you want, but as far as I know, no one has ever used the Curry-Howard toolbox to solve a nontrivial algorithmic problem for the first time. Any exciting paper about algorithms (like quicksort, Dijkstra's algorithm, or Primes in P) will usually have a lot of math involving numbers, but no math involving types.
<i>"In this sense all three have ontological force; they codify what is, not how to describe what is already given to us."</i><p>What's the difference between "what is" and "what is already given to us"? What's the difference between codifying and describing it?
What a coincidence... just ran across this video -- <a href="https://www.youtube.com/watch?v=YRu7Xi-mNK8" rel="nofollow">https://www.youtube.com/watch?v=YRu7Xi-mNK8</a> -- last night, where Prof. Frank Pfenning makes a similar point in the first few minutes.
How is this going to make my code better?
As far as I remember attempts to use proofs in production were counter productive.
For most systems knowing that print "hello"; will do that is good enough.