4 ms·
The "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
by ulrikrasmussen 6y ago
The "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 6y 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.)