I’m not sure those famous math papers apply here - while programs can be proofs, they in general occupy a much larger category, don’t they?
Calculable functions quickly “outgrow” mathematics.
I mean the Curry-Howard-Lambek correspondance is that lambda calculus, proofs/logic and category theory are all just different ways of talking about the same thing for the most part
We’re not talking about trying to prove correctness; this is about the representational semantics of the language (a symbol system) itself.