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?
