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.
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.