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

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.