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?

I don't know. You could equally argue (at least to a judge) that everything that can be coded in binary is actually an integer.

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.