Je ne vois pas en quoi un langage non Turing-complet ne serait pas un langage de programmation. Obtenir un langage utilisable1 qui se trouve du bon côté de la frontière de Turing, derrière laquelle c'est le chaos (on ne sait presque plus rien dire du comportement des programmes), est justement une grande victoire des types dépendants.
1: à discuter. Mais plus utilisables que tout ce qu'on faisait avant dans le genre
Pour moi, la construction d'automates pour calculer des propriétés de mots (le modulo deux d'un nombre binaire par exemple) est aussi une forme de programmation, bien que ce ne soit pasnon plus Turing-complet.
[^] # Re: Différents langages
Posté par gasche . En réponse à la dépêche Apprendre un langage de programmation par an. Évalué à 1.
1: à discuter. Mais plus utilisables que tout ce qu'on faisait avant dans le genre
Pour moi, la construction d'automates pour calculer des propriétés de mots (le modulo deux d'un nombre binaire par exemple) est aussi une forme de programmation, bien que ce ne soit pasnon plus Turing-complet.