3 ms·

I'm very confused about what this blog post is trying to argue. Most of what it discusses isn't related to the Curry-Howard correspondence at all? At the risk

• uryga 7y ago
  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)
• jrsala 7y ago
  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.