4 ms·
Programs ARE proofs. The types are logical propositions. If the code runs then the propositions are true, although for most programming languages types are very
by proc0 3y ago
Programs ARE proofs. The types are logical propositions. If the code runs then the propositions are true, although for most programming languages types are very flexible so from the mathematical perspective they aren't proving anything interesting (even though the program is doing something useful). This is the Curry-Howard correspondence between logic and programs: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
- AnimalMuppet 3y agoIf the program can do something useful while not proving anything interesting, then no, programs are not proofs.
- baremetal 3y agoProving is objective. Interesting is subjective. Your conclusion doesn't follow from the premises.
- AnimalMuppet 3y ago"Interesting" is subjective. So is "useful". I assert that a useful program is more interesting than a useless one. If it's useful (and interesting) as a program, and uninteresting as a proof, then there is a difference between proofs and programs, not at the level of the Curry-Howard Correspondence, but at the level of human life. As a program it can make your life easier; as a proof it's not going to change anyone's life in any way whatsoever.
- kazinator 3y agoPrograms in a tiny academic bubble are proofs, where types are logical propositions.
- deleted 3y ago[deleted]