I've noticed that the kinds of things a mathematician might pride an elegant proof over are the same kinds of things a programmer might recognize as elegance in

I've noticed that the kinds of things a mathematician might pride an elegant proof over are the same kinds of things a programmer might recognize as elegance in code as well. I think the Curry-Howard Correspondence is actually an intuitive result rather than a surprising one, and that any experienced programmer who understands formal proofs as well as they understand computer programming would eventually arrive at the Correspondence on their own, or at least a suspicion of it.