Cubical Agda is an example of a "programming language" which uses HoTT features: https://agda.readthedocs.io/en/v2.6.0/language/cubical.html https://agda.readth

Cubical Agda is an example of a "programming language" which uses HoTT features: https://agda.readthedocs.io/en/v2.6.0/language/cubical.html https://agda.readthedocs.io/en/v2.6.0/language/cubical.html It's actually a proof assistant, but you can still write code in it - and perhaps even export it to code in other languages. Regarding the "smart" features you suggested, those sound interesting, but I'm not aware of any language having them. Could be useful.