2 ms·
> It's pretty simple: due to Curry-Howard isomorphism, programming languages are just notations for some type of formal logic. Thank you, this made me chuckle!
by tucnak 16d ago
> It's pretty simple: due to Curry-Howard isomorphism, programming languages are just notations for some type of formal logic.
Thank you, this made me chuckle!
- js8 15d agoNot really sure if it's sarcasm, but let me make a side remark. It's really stunning how much more effective the "Standard ML" notation (embraced by Haskell, Lean etc.) is compared to writing proofs in classical logic. This "UX problem" is, I think, the reason why is mathematical community embracing automated provers maybe 50 years later than they could have. Automated people wanted the better language, but the mathematicians largely resisted. So seeing this, it would be preposterous for me to think that any language, natural or not, has the last say in this. We're gonna be stuck with learning new languages and formalisms for a long time.