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.