I'm not sure either of us really knows how Curry-Howard works, but my understanding is that it's a compile-time type system thing. In certain proof languages, a function that returns an int proves that an int exists (type is inhabited). And that's just not very interesting - you need more sophisticated types than we commonly use. Also, it only works for total functions, so it's not true in most ordinary programming languages.

So I'm skeptical that the code we write in ordinary programming languages proves anything interesting. Why do you think that?