Liam O'ConnorI had an extremely frustrating exchange with a FP practitioner who was overly enthusiastic about Curry-Howard the other day, so I tried to write up my thoughts in this note here.
mb21@liamoc Seems the question “programs are proofs, yes, but proofs about what?.” wasn’t really answered? Or did I miss it somehow? Would love an example.
@mb21 it is; the answer is that they're proofs of abstract logical sentences in propositional or second-order logic.
@mb21 Viewed from a traditional logical lens, the types (32-bit) Int and Bool are both just true, albeit with 2^32 and 2 witnesses to that truth respectively. So, I guess, assuming true, we have true? It's a very pointless logical proposition to prove. The value of the type doesn't come from its logical interpretation here.
Robin Adams@robinadams @mb21 Right -- it's even a stretch to say that "Int" is a proof that there exists an integer, in the traditional sense (∃ x. x ∈ ℤ). Rather it is a true proposition with |ℤ| many different witnesses to its truth. The notion of something being an integer or a boolean doesn't exist in the logic.