>all mathematical proofs are actually programs

This is not true. Only a subset is stated by Curry-Howard correspondence.