3 ms·
Proving is objective. Interesting is subjective. Your conclusion doesn't follow from the premises.
by baremetal 3y ago
Proving 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.