As much as the concept blew me away when I first heard of it, I can't shake the feeling that the Curry-Howard correspondence is somehow mis-marketed as something that would immediately cater to programmers. The idea to encode propositions into types sounds enticing for programmers, because there are indeed a lot of cases where something needs to be conveyed that can't be conveyed using type systems (or other features) of common programming languages.
Examples include the famous "the caller of this function guarantees that the argument is a non-empty list" but also "the caller guarantees that the argument object has been properly locked against concurrent access before using the function".
However, in my experience, the community is more interested in mathematics than in programming and I don't know if anybody is really working to provide propositions-as-types to mainstream programmers. This is certainly because it is hard enough to prove soundness of a strict functional programming language as Agda or Rocq, much more for anything imperative, stateful, "real-world", non-strict, non-pure, concurrent, ill-defined, you name it.
So, for me the promise of "showing programmers that what they do is actually mathematics" is not really kept as long as the definition of "programmer" is so narrow that it excludes the vast majority of people who define themselves as programmers.
What I'm trying to say: I wish there were more efforts to bring more powerful formal methods, especially as powerful as dependent types, to existing mainstream programming languages where they could be useful in an industrial context. Or at least try to come up with new programming languages that are more pragmatic and do not force the programmer into some narrow paradigm.
Am I wrong? I hope so :)
The author has given a few talks built around the same concept: https://www.youtube.com/watch?v=IOiZatlZtGU
Slightly OT: I'm a master's student in computer science who focuses mostly on machine learning. Still, the best course I've ever taken was one on semantics and types, presenting many of the ideas in this article. Learning proof-writing using natural deduction with a ruthlessly rigorous teacher has made me much more precise when I write proofs in general, and learning about theory of computation and logic has given me a good mental model of how my programs execute.
While the course is an elective mostly focused on students interested in programming languages, I think all computer scientists can benefit from taking such a course. In a time where everyone wants to do AI, the course only had around 12 students out of a class of maybe 200 students.
Even more OT: Phil Wadler gave a talk at the programming language section of my university not too long ago, which I was much excited to see. Sadly, he chose a vague pop-sciency talk on AI which felt quite a bit outside his expertise.
Related (I think) - others?
Propositions as Types: Explained (and Debunked) - https://news.ycombinator.com/item?id=38894706 - Jan 2024 (1 comment)
Propositions as Types - https://news.ycombinator.com/item?id=17947379 - Sept 2018 (1 comment)
Propositions as Types (2014) [pdf] - https://news.ycombinator.com/item?id=10553766 - Nov 2015 (6 comments)
On Propositions as Types [video] - https://news.ycombinator.com/item?id=10154349 - Sept 2015 (3 comments)
I really recommend [56] M. H. Sørensen and P. Urzyczyn. Lectures on the Curry-Howard isomorphism. Elsevier, 2006 on this topic. I found it online.
It is very self-contained and explains some interesting topics such as relation of intuitionist and classical logic.
I dont want to prove that my code is correct.
I would prefer to create specifications in logic and have the code derived for me.
Other than something like Prolog, are there tools for working this way?
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.
Could have written further into set theory and set theoretic interpretation of types.
A proposition being a set intension.
I feel like every time I try to do super formal proofs for code, it ends up way more brutal than I expect and slower than just fixing stuff as I go. Still love types catching my mess-ups for me though.
In my opinion it's a tragedy there are so few resources in using "Propositions as Types"/"Curry–Howard correspondence"[0] in didactics in tandem with teaching functional programming to teach structured proof-writing.
Many students do not feel comfortable with proof-writing and cannot dispatch/discharge implications or quantifications correctly when writing proofs and I believe that a structured approach using the Curry-Howard correspondence could help.
[0]: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...