The Curry-Howard isomorphism (types are theorems, programs are proofs)

Doesn't this sort of thing put lie to the idea of patenting algorithms, as mathematics is unpatentable, types are theorems and programs are proofs?

Cool.

I'm also a fan of intuitionist logic in the context for this discussion, because uninhabited but "true" types such as ((a -> b) -> a) -> a are not theorems.