Most overrated correspondence ever. You don't need curry-howard for software verification, you don't need it for mathematics, and you don't need it for logic.

Most overrated correspondence ever. You don't need curry-howard for software verification, you don't need it for mathematics, and you don't need it for logic. You only really need it to j*rk off hard over types.