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?"
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?