[lightsighter]

All programs are proofs and their results are theorems[1]. If "math is naturally inherent and merely discovered by humans" then so are all programs; programmers are just discoverers and not inventors. Given the proof of Curry-Howard Isomorphism rests on existing maths we can have another discussion about whether mathematical patents should be issued if we don't believe that maths are inherent and are actually invented, but as long as we hold that we can't patent maths then it must also hold that we can't patent programs due to their equivalence. [1]: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

[yorwba]

Programs and proofs are not actually equivalent. The Curry-Howard correspondence is only concerned with the types. If you take a useful program and replace every function with another of the same type, the program is now pointless but still corresponds to the same proof. And unless you're explicitly trying to encode mathematical statements into the type system, that proof is likely to only show something trivial like "there is an integer".