The Curry-Howard correspondence seems like one of those things that's weird and unexpected but not actually very useful?
Most of the types that correspond to propositions, and programs that correspond to proofs, aren't of much utility in actual programming. And most of the useful programs and their types don't correspond to interesting proofs and propositions.
The paper relates it to other connections between fields, such as Cartesian coordinates linking geometry and algebra. This allows you to bring the power of algebra into geometric problems and geometric intuition into algebra problems. But does the Curry-Howard correspondence bring similar powers?
--
This kind of rearrangement without really changing anything reminds me of the equivalence between first-order logic terms and sets. Consider [P] to be the set of models where statement P is true - then [A∧B] = [A]∩[B], [A∨B] = [A]∪[B] and so on. But this doesn't lead to any new insights. You basically just wrote the same thing with different symbols.
In some contexts (proving soundness/completeness) it can allow you to step down one turtle, but you still have aleph-null turtles below you so that doesn't seem that useful either.
I’m not a mathematician but I’ve heard that the topics that lead to modern cryptography was once considered absolutely useless. They say for centuries, number theory (especially areas like prime numbers, modular arithmetic, and whatnot) was seen as the peak of “pure” math with no real world utility.
Personally, im all for static analysis and formal verification in software, particularly the kind where properties can be automatically verified by a computer and to my understanding this field is the on bleeding edge of what’s possible.
From a big picture perspective, our world is dependent on software, lives can be at risk when software fails, so for this reason I think its worthwhile to explore ideas that may one day lead to inherently more robust software even if it’s comercial utility isn’t clear.
Most of the types that correspond to propositions, and programs that correspond to proofs, aren't of much utility in actual programming. And most of the useful programs and their types don't correspond to interesting proofs and propositions.
The paper relates it to other connections between fields, such as Cartesian coordinates linking geometry and algebra. This allows you to bring the power of algebra into geometric problems and geometric intuition into algebra problems. But does the Curry-Howard correspondence bring similar powers?
--
This kind of rearrangement without really changing anything reminds me of the equivalence between first-order logic terms and sets. Consider [P] to be the set of models where statement P is true - then [A∧B] = [A]∩[B], [A∨B] = [A]∪[B] and so on. But this doesn't lead to any new insights. You basically just wrote the same thing with different symbols.
In some contexts (proving soundness/completeness) it can allow you to step down one turtle, but you still have aleph-null turtles below you so that doesn't seem that useful either.