pacjo@lemmy.dbzer0.com to Piracy: ꜱᴀɪʟ ᴛʜᴇ ʜɪɢʜ ꜱᴇᴀꜱ@lemmy.dbzer0.comEnglish · 9 months agoI absolutely love VideoLAN's stance regarding patentslemmy.dbzer0.comimagemessage-square65fedilinkarrow-up1852arrow-down110
arrow-up1842arrow-down1imageI absolutely love VideoLAN's stance regarding patentslemmy.dbzer0.compacjo@lemmy.dbzer0.com to Piracy: ꜱᴀɪʟ ᴛʜᴇ ʜɪɢʜ ꜱᴇᴀꜱ@lemmy.dbzer0.comEnglish · 9 months agomessage-square65fedilink
minus-squareGeniusIsme@lemmy.worldlinkfedilinkEnglisharrow-up13arrow-down4·9 months agoProofs can be represented as programs, not the other way around. Also, USA allows for algorithm parents, and algorithms are maths. While I agree with you, your reasoning is not correct.
minus-squarehglman@lemmy.mllinkfedilinkEnglisharrow-up11arrow-down1·9 months agoNo, the proof - program correspondence is in both directions.
minus-squareGeniusIsme@lemmy.worldlinkfedilinkEnglisharrow-up3arrow-down3·9 months agoCorrespondence is quite a weak relation. Very far from one being another.
minus-squarelad@programming.devlinkfedilinkEnglisharrow-up2·9 months agoI’d say if you ask a mathematician, they would disagree with you. But maybe that depends on how far they have gone into maths from common sense
minus-squarenakal@kbin.sociallinkfedilinkarrow-up1·9 months agoThat’s why it’s also called Curry-Howard isomorphism.
Proofs can be represented as programs, not the other way around. Also, USA allows for algorithm parents, and algorithms are maths. While I agree with you, your reasoning is not correct.
No, the proof - program correspondence is in both directions.
Correspondence is quite a weak relation. Very far from one being another.
I’d say if you ask a mathematician, they would disagree with you. But maybe that depends on how far they have gone into maths from common sense
That’s why it’s also called Curry-Howard isomorphism.