this post was submitted on 21 Dec 2023
1041 points (99.0% liked)

Piracy: ꜱᴀɪʟ ᴛʜᴇ ʜɪɢʜ ꜱᴇᴀꜱ

54424 readers
409 users here now

⚓ Dedicated to the discussion of digital piracy, including ethical problems and legal advancements.

Rules • Full Version

1. Posts must be related to the discussion of digital piracy

2. Don't request invites, trade, sell, or self-promote

3. Don't request or link to specific pirated titles, including DMs

4. Don't submit low-quality posts, be entitled, or harass others



Loot, Pillage, & Plunder

📜 c/Piracy Wiki (Community Edition):


💰 Please help cover server costs.

Ko-Fi Liberapay
Ko-fi Liberapay

founded 1 year ago
MODERATORS
 
you are viewing a single comment's thread
view the rest of the comments
[–] [email protected] 11 points 10 months ago (1 children)

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.

[–] [email protected] 13 points 10 months ago (1 children)

No, the proof - program correspondence is in both directions.

[–] [email protected] -2 points 10 months ago (3 children)

Correspondence is quite a weak relation. Very far from one being another.

[–] [email protected] 2 points 10 months ago

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

[–] [email protected] 1 points 10 months ago

Correspondence is not correlation.

[–] [email protected] 1 points 10 months ago

That's why it's also called Curry-Howard isomorphism.