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.
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.
Correspondence is not correlation.