The Curry-Howard isomorphism doesn't say that an interesting proof corresponds to a program anyone would care about (other than as an equivalent to the proof),

The Curry-Howard isomorphism doesn't say that an interesting proof corresponds to a program anyone would care about (other than as an equivalent to the proof), nor that an interesting program corresponds to a proof anyone would care about (other than as an equivalent to the program). In practice, writing programs and finding proofs feel like quite different activities, and at least in my experience of doing both I almost never try to write a program by thinking "how could I prove that such-and-such a type is nonempty" and I literally never try to prove something by finding a corresponding type and writing a program that computes or represents something of that type. The Curry-Howard isomorphism is a beautiful theorem, and as you say it inspires some nice methods of automated proving / proof-checking, but I don't think it says anything much about the relationship between the programming and theorem-proving activities that actual humans engage in.