I also still don't get it, years later. I wrote a short post on this (a bit too inflammatory, tbh, sorry for the URL): https://blag.cedeela.fr/curry-howard-scam

I also still don't get it, years later. I wrote a short post on this (a bit too inflammatory, tbh, sorry for the URL): https://blag.cedeela.fr/curry-howard-scam/ https://blag.cedeela.fr/curry-howard-scam/ . A lot of logic and theorem proving can be done without ever thinking about CH. In classical logic I think it's not even that convenient anyway, and classical logic is a pragmatic choice.