People in the very theoretical end of programming language research seem to be makingnoise about something called homotopy type theory, that’s supposed to make programming awesome and machine-provable once someone gets around to implementing it.
Like the lambda calculus before it (which is actually embedded in it), MLTT may be a fruit of mathematics that has a very real and practical impact on how programmers think about programming. It could be the unifying paradigm that eventually, finally puts an end to all the “programming language wars” of our time. Already it has begun to transform the mathematical community.
It’s apparently related to intuitionistic type theory, which one researcher is also very enthused about:
Intuitionistic type theory can be described, somewhat boldly, as a fulfillment of the dream of a universal language for science. In particular, intuitionistic type theory is a foundation for mathematics and a programming language.
Does anyone who has some actual idea what’s going on here have an opinion on this?
You seem to be confusing intuitionist MLTT (c.1970) and HTT (c.2005). Your second and third links are about MLTT, not HTT. The second link does mention HTT in passing and claims that it is “a new interpretation of type theory,” but this is simply false. In particular, your first quote is not about HTT.
Your first link really is about HTT, but does not claim that it is relevant to programming. HTT is an extension of type theory to reduce the impedance mismatch between logic and category theory, especially higher category theory. It is for mathematicians who think in terms of categories, not for programmers. In as much as programmers should be using category theory, HTT may be relevant. For example, Haskell encourages users to define monads, but does not require them to prove the monad laws. HTT provides a setting for implementing a true monad type, but is overkill. This is largely orthogonal to MLTT.
Automated theorem proving is rarely done, but it usually uses MLTT.
You are of course right about the distinction between MLTT and HTT, but Risto_Saarelma’s first link is a computer science blog. In my view, the claim that computer scientists are “making noise” about homotopy type theory as applicable to programming is fairly justified: in particular, HTT might make it easier to reason about and exploit isomorphisms between data types, e.g. data representations.
Also, Martin-Lof type theory is not exclusively used for computer-assisted theorem proving: for instance, the Calculus of Constructions is one alternative. Formal work on HTT is done in Coq, which is based on the CoC.
People in the very theoretical end of programming language research seem to be making noise about something called homotopy type theory, that’s supposed to make programming awesome and machine-provable once someone gets around to implementing it.
It’s apparently related to intuitionistic type theory, which one researcher is also very enthused about:
Does anyone who has some actual idea what’s going on here have an opinion on this?
You seem to be confusing intuitionist MLTT (c.1970) and HTT (c.2005). Your second and third links are about MLTT, not HTT. The second link does mention HTT in passing and claims that it is “a new interpretation of type theory,” but this is simply false. In particular, your first quote is not about HTT.
Your first link really is about HTT, but does not claim that it is relevant to programming. HTT is an extension of type theory to reduce the impedance mismatch between logic and category theory, especially higher category theory. It is for mathematicians who think in terms of categories, not for programmers. In as much as programmers should be using category theory, HTT may be relevant. For example, Haskell encourages users to define monads, but does not require them to prove the monad laws. HTT provides a setting for implementing a true monad type, but is overkill. This is largely orthogonal to MLTT.
Automated theorem proving is rarely done, but it usually uses MLTT.
You are of course right about the distinction between MLTT and HTT, but Risto_Saarelma’s first link is a computer science blog. In my view, the claim that computer scientists are “making noise” about homotopy type theory as applicable to programming is fairly justified: in particular, HTT might make it easier to reason about and exploit isomorphisms between data types, e.g. data representations.
Also, Martin-Lof type theory is not exclusively used for computer-assisted theorem proving: for instance, the Calculus of Constructions is one alternative. Formal work on HTT is done in Coq, which is based on the CoC.