C-H isn't useful to programmers at all. The programs that represent proofs end up being useless programs, most of the time, and the proofs represented by real-w

C-H isn't useful to programmers at all. The programs that represent proofs end up being useless programs, most of the time, and the proofs represented by real-world programs end up being useless proofs, most of the time. Most programs deal with several objects of the same type - your program probably contains more than one integer (shocking, right?). Since C-H maps each unique type to a unique proof term, the same type maps to the same proof term. A function that calculates greatest common factor of two numbers proves that (A∧A)→A, or "(A and A) implies A" which is... uninteresting. In the reverse direction, the program generated by (A∧A)→A is either the first or second entry selector from a tuple, and doesn't calculate the greatest common factor of two integers. (A∨A)→A is slightly more interesting, taking Either<int, int> and returning int. It's true that C-H of logical disjunction gives you Either types, conjunction gives you tuple types, and implication gives you function types. Kinda fascinating, enough to write a blog post about, but still without any practical purpose. Practical types with additional requirements (such as non-empty lists) have nothing to do with C-H and could exist even if C-H were false. Same for dependent types. As I said, C-H is completely useless in actual programming. I do wish we had more formal methods though. Formal methods of programming have nothing to do with C-H either. Static typing has nothing to do with C-H. The Rust borrow checker has nothing to do with C-H. Complete formal verification (as in seL4) has nothing to do with C-H.