[cousin_it]

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.

[s-phi-nl]

Could you point to a reference for the non-confluence of logic without excluded middle? It sounds interesting and a quick Google search did not find anything.

[cousin_it]

With excluded middle. This is the explanation that clicked for me: http://stackoverflow.com/questions/24711643/how-come-that-we...

[s-phi-nl]

Thanks! Yes, with excluded middle is what I meant.