3 ms·

I used to be absolutely against software patents on those grounds, but I nowadays actually think it's a weak argument. We don't see people arguing we shouldn't

I used to be absolutely against software patents on those grounds, but I nowadays actually think it's a weak argument. We don't see people arguing we shouldn't patent physical machines because ultimately each operation is a simple physical movement, so the sum of everything is just a sequence of physical movements. Yet we see people arguing we shouldn't patent software "machines" because ultimately each operation is a simple mathematical operation, so the sum of everything is just a sequence of mathematical operations. The argument against the patentability of maths, AFAIK, has always been "maths is naturally inherent and merely discovered by humans". This, to me, is an argument against pure maths especially; but as we get into applied maths I think it's much less arguable that algorithms and data structures are naturally inherent (much like how physical constructions—machines—aren't naturally inherent from the laws of physics). I still strongly think far too many patents get issued, but I'm less convinced than I used to be software patents are inherently bad, and that patents do need reform in various ways.

lightsighter 8y ago
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_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
- yorwba 8y ago
  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".
brlewis 8y ago
>I still strongly think far too many patents get issued Then you are against software patents. If millions of people carried machine shops around in their backpacks, you would be against mechanical engineering patents, because far too many patents would be issued. At the core of patent law is "presumption of validity", which places the burden of proof on the accused, rather than the accuser. Anything that multiplies the number of patents the PTO has to examine makes that presumption less reasonable. At some point it's arguable that a party accused of patent infringement is not getting due process. Software patents. Presumption of validity. Due process. Choose any two.

lightsighter 8y ago

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_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

yorwba 8y ago
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".

brlewis 8y ago

>I still strongly think far too many patents get issued Then you are against software patents. If millions of people carried machine shops around in their backpacks, you would be against mechanical engineering patents, because far too many patents would be issued. At the core of patent law is "presumption of validity", which places the burden of proof on the accused, rather than the accuser. Anything that multiplies the number of patents the PTO has to examine makes that presumption less reasonable. At some point it's arguable that a party accused of patent infringement is not getting due process. Software patents. Presumption of validity. Due process. Choose any two.