En effet, une sémantique formelle simple et des preuves mécaniques simples ça ne veut pas forcément dire intuitives pour l'humain : il suffit d'avoir un peu utilisé un assistant de preuve comme Coq pour s'apercevoir que notre vision du simple et du compliqué est souvent en désacord avec celle de la machine. Ceci dit, je dirais quand même qu'en pratique, dans le doute, viser une sémantique formelle simple et adaptée raisonnements formels a des chances d'aider à obtenir un langage plus simple pour l'humain aussi (l'idéal étant d'avoir les deux); et puis je dirais rajouter des irrégularités que lorsqu'on a une bonne raison, comme par exemple viser à être moins général et utiliser une solution plus ad hoc lorsque c'est plus raisonnable d'un point de vue humain.
[^] # Re: Le cerveau n'est pas logique
Posté par anaseto . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
En effet, une sémantique formelle simple et des preuves mécaniques simples ça ne veut pas forcément dire intuitives pour l'humain : il suffit d'avoir un peu utilisé un assistant de preuve comme Coq pour s'apercevoir que notre vision du simple et du compliqué est souvent en désacord avec celle de la machine. Ceci dit, je dirais quand même qu'en pratique, dans le doute, viser une sémantique formelle simple et adaptée raisonnements formels a des chances d'aider à obtenir un langage plus simple pour l'humain aussi (l'idéal étant d'avoir les deux); et puis je dirais rajouter des irrégularités que lorsqu'on a une bonne raison, comme par exemple viser à être moins général et utiliser une solution plus ad hoc lorsque c'est plus raisonnable d'un point de vue humain.