[jrsala]

I think in the context of the author's field, an enlarged definition of the notion of "propositions" is adopted whereby a proposition is a useful statement about the real world, distinct from, but related to the mathematical definition of a formal object used for reasoning about some notion of truth.

The author's point in part 1 is that type systems are intrinsically incapable of formalizing propositions so as to achieve the holy grail of making software systems effective, safe, or whatever other property is sought after, in the real world. The author then goes on to explain this idea and to suggest a different approach.

As for the Curry-Howard isomorphism, the author does say it is perfectly valid from a mathematical point of view, but that is not the subject of the text.