Existe-t-il des langages de spécification lisible par machine (et humain) pour les collections d'algorithmes et les méta-bibliothèques?

Question

Existe-t-il un langage de haut niveau pour décrire les algorithmes, orienté vers la spécification plutôt que vers la mise en œuvre?

L'idée serait d'avoir une archive lisible par machine des algorithmes standards, avec des annotations lisibles à la machine sur des arbitrages et des variantes.

Je pense à quelque chose comme CycL/OpenCyc, mais pour les algorithmes et modèles de programmation.

Answer 1

La réponse facile: Oui. Ça s'appelle anglais.

La réponse sérieuse: Non, comme vous l'avez probablement déjà pris après des mois de cette question sans réponse allant. Je ne crois pas qu'il y ait vraiment de consensus, ni même de considération, sur ce que cela impliquerait. Les schémas de programmation et les algorithmes évoluent et évoluent constamment, donc concevoir un langage capable de décrire tous les modèles futurs serait très difficile, voire impossible.

Answer 2

pseudocode, peut-être. Ou des organigrammes. Pour une machine lisible, il faudrait que ce soit quelque chose comme un méta-langage. Lisp et Forth me viennent à l'esprit. Des langages qui se définissent essentiellement eux-mêmes, avec un petit ensemble de primitives pour construire les couches supérieures de l'abstraction.

Answer 3

Ce ne sont pas des ajustements précis, mais ils sont assez proches: Maude et CASL. Ils sont tous les deux des langages de spécification lisibles par machine (avec des outils décents) qui permettent également certaines formes de code. Certaines personnes ne jurent que par AsmL, mais je ne suis pas fan.

Bientôt, je pense que Agda 2 va très bien remplir ce créneau, mais il est encore en plein développement. On peut aussi dire que Coq remplit déjà ce rôle (à cause de l'extraction de programme), mais je ne suis pas non plus un fan.