Unifying Programming and Math – The Dependent Type Revolution

The way that programmers and mathematicians work seems to be very different. Programming is about making computers do something, whereas math is about describing things. Programming involves state that changes over time, whereas math deals with Platonic theorems that are always true, even if not proven yet.

But, in fact, the Curry-Howard Isomorphism states that there is a very direct correspondence between basic logical concepts (namely, propositions) and basic programming concepts (namely, types). This correspondence has been known for a long time, but it is only recently that it has begun to creep into the actual practices of programmers and mathematicians alike.

Due to a recent advance in mathematics called Homotopy Type Theory, programming and math are about to be unified on a practical level in a way that will fortify their strengths and overcome some of their respective weaknesses.   Read more on Unifying Programming and Math – The Dependent Type Revolution…