yeah, Ctrl+F "type" gives 4 (non-title) occurrences, all of them in the first two paragraphs. the rest seems to be related to AI and the problems of making it "actually refer to the real world". weird!
EDIT2: i think the author is actually talking about cogsci "mental propositions". (see my other comment)
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.
At the risk of sounding anti-intellectual, perhaps Orwell's "Politics and the English Language" [0] is relevant here?
[0] http://www.orwell.ru/library/essays/politics/english/e_polit