5 ms·
By Curry-Howard, the program is the proof, albeit usually not of an interesting proposition.
by mafribe 11y ago
By Curry-Howard, the program is the proof, albeit usually not of an interesting proposition.
- groar 11y agoIn a rich type system, a program is the proof of its own specification. Which is usually as interesting as the program itself.
- mafribe 11y agoSure, but as of July 2015 the programming languages (e.g. Agda, Idris) that can give full specifications of their own programms, are experimental, not mainstream.
- black_knight 11y ago«Which is usually as interesting as the program itself.» And ten times as hard to write. Not just saying that — I spend most of my time in Agda, and even simple things are rather difficult. But I think this will improve as we learn the right way to look at things.
- im3w1l 11y agoBottom is a member of every type, so all Haskell programs correspond to proofs of trivial propositions. Or that is my understanding anyway. And something similar should be true for common imperative languages.
- tel 11y agoNot quite. Bottom as a member of every type means that you cannot trust my proof (x : A) without examining it and that your examination may be non-terminating. That said, it you examine a realizer and terminate then you have a genuine proof of a potentially non-trivial theorem. The reason why most Haskell theorems are trivial is because lacking dependent types means that we cannot ask for interesting theorems. `3 :: Int` is a perfectly nice proof that "Integers exist" which is a little silly.