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 […]