At a technical level, I understand the Curry-Howard correspondence in various settings, and its usefulness as a technical tool. What I'm looking for is a fairly rigorous discussion of genuinely philosophical consequences of the CH correspondence. So, for example, does the resulting 'propositions as types' slogan just mean that propositions can be represented as types, or that propositions really are types?
The literature is full of computer scientists making vague and not especially precise claims about the philosophical significance of the CH correspondence, but frankly I find most of these discussions very casual and sloppy. Is there a non-trivial, substantive philosophical claim about the nature of proofs or propositions that flows naturally from the CH correspondence? Even just references to good literature would be helpful.