Evolving the Industry Unifying Programming and Math – The Dependent Type Revolution A programmer's introduction to Martin-Löf Type Theory, a recent theory that elegantly unifies programming and math.
