Homotopy type theory is a programming language whose original purpose was "math-as-code". Gaining widespread adoption among mathematicians, let alone programmers, seems unlikely as mathematicians dislike programming languages for their perceived lack of elegance and are firmly set in their set theoretic ways, while most programmers balk at the barest hint concision and rigor.
HoTT isn't a programming language, because there are non-value normal forms. That's the whole reason behind research into various formulations of Cubical Type Theory, which is a programming language.
Intensional intuitionistic type theory is a programming language. Throw in higher inductive types (still a programming language at this point) and Voevodsky's univalence and you've got HoTT. Then sure, the simplicial model is not constructive, whereas the cubical models give computational meaning to univalence, but they're still just that, models of HoTT. So would you prefer I had said HoTT has models that are programming languages?
