Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

What is commonly known as Curry-Howard correspondence (the duality between programs/proofs, computing/math) actually goes way deeper.

The reason is that "computation" is very useful concept but it has taken us ages to define what it means precisely. But that didn't stop people of reinventing it in other areas.

Curry-Howard is only one of many other isomorphism between programs and other areas. See "Physics, Topology, Logic and Computation: A Rosetta Stone"[1] and in particular Table 4 on pg. 66. Curry-Howard correspondence is the last two columns of the table; the other three columns are other "correspondences" in topology, physics and category theory.

[1] http://math.ucr.edu/home/baez/rosetta.pdf



Guess I'll not be a coward & hurry! To study Howard & Curry.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: