Per VognsenI've seen several independent, complete misconceptions of the Curry-Howard isomorphism just in the last week. Where are people getting these ideas, I wonder. Today's specimen, courtesy of the Hegel thread on HN: "Given Curry-Howard isomorphism, couldn't we ask AI to directly prove the property of the binary executable under the assumption of the HW model, instead of running PBTs?"
I normally never read HN but a specific thread was linked in the Hegel thread on Lobsters, so I guess I brought it upon myself for clicking through that link.
Wolf480pl@pervognsen Did the HN poster somehow think that Curry-Howard isomorphism will make modelling the HW, the program, and the desired properties in a formal proof language like coq or Agda somehow easier?
Brad Larsen@pervognsen yes!! I saw that comment too and thought to myself that the commenter should put down the crack pipe. Big words but a completely ridiculous question that belies either trolling or a total misunderstanding of all of it. LLM commentary perhaps? It's an old account though.