Perhaps this is just a skill issue, but I’ve seen a lot of good programmers get CH-pilled and then waste a lot of time trying to think of the types of their working programs as rich propositions or trying to encode complex proofs about their programs in the types.
The Curry-Howard correspondence is only one of many lenses we can use to view the relationship between things and facts. Different lenses characterize different approaches to foundation:
- Propositions are basic (single-sorted logics, ZF)
- Types are basic, some types are propositions (Homotopy Type Theory)
- Propositions and types are the same (Martin-Löf’s Type Theory)
- Propositions and types are different but equally basic (Logic-enriched Type Theory)
Shulman explains how the Axiom of Choice is true some but not in others, arguing that in certain respects, the HoTT’s way is the most “natural”: golem.ph.utexas.edu/category…
Adams & Luo argue instead for the practical virtues of making propositions and types completely separate: arxiv.org/html/0809.2061v3
9
1
38
7,504
A subset of developers love the puzzle of types, how do you map something to that world. These are the people who self select into it. Rust also has its version of this where doing basic efficient concurrency is so hard that people write thesis about it, but they like it
Sep 24, 2026 · 5:24 PM UTC
1
219