3 ms·
According to Curry-Howard correspondence, writing programs is like writing proofs. So a working (or at least type-checked) program is like a proof that was veri
by js8 7y ago
According to Curry-Howard correspondence, writing programs is like writing proofs. So a working (or at least type-checked) program is like a proof that was verified by the computer.
In that sense, the poorly understood ideas have to be expressed more precisely, when writing a program. The program itself, however, is not necessarily a good medium to express the most interesting ideas, because they can drown in technical details.
- justinmeiners 7y agoJust because the program corresponds to a proof, doesn't mean it proves anything interesting. It may not give any insight into the subject you're trying to understand
- ulrikrasmussen 7y agoThe "propositions" that are proved in anything but dependently typed languages are trivial though, so Curry-Howard is not that relevant in this context. E.g. a program of type "Int" merely proves that the set of integers is non-empty, and it doesn't even prove that for languages that are Turing complete (as the "proof" may crash)
- js8 7y agoThat's why I used phrase "working program" and "verified" in my comment. ;-) If you have a working (tested) program, you might not have a mathematical proof that it works, but you have certain sense that what you're doing is not entirely logically implausible. It is a form of verification (although without complete guarantee of correctness). (Another way to look at it is that the testing you did determines what kind of sentence you proved to be true. So instead of assigning the type to the program in advance, you deduce it the other way around - we observe how the program works and that gives us its type.)
- auggierose 6y agoYeah, that's why I call bullshit on Curry-Howard. It's really not that important or noteworthy. Writing down a program is not like writing down a proof. It is like writing down a specification.