L'idée est d'utiliser la correspondance de Curry-Howard.
En math, on démontre souvent des trucs du genre: A implique B.
En info, on code souvent des fonctions qui prennent A et qui rendent B.
Si on réinterprète les maths, le théorème A implique B, ce n'est rien d'autre qu'une fonction qui, à partir d'une preuve de A, te rend une preuve de B. C'est la même chose.
En brodant un peu (beaucoup), on obtient un truc comme COQ qui permet de générer du code certifié. La seule chose, c'est que le mode de programmation est carrément spécial.
Exemple, pour programmer un tri, on démontre le théorème suivant:
Il existe une fonction f de l'ensemble des listes dans l'ensemble des listes telle que
- f(l) est une permutation de l
- f(l) est triée.
Une fois le théorème démontre, on peut demander à COQ de sortir du code implémentant une fonction qui vérifie les hypothèses du théorème: un tri.
Bref, le jour où les programmeurs de base sauront utiliser ce genre d'outil n'est pas encore arrivé.
[^] # Re: Les mathématiques Formels
Posté par fmaz fmaz . En réponse au journal L'expressivité des langages. Évalué à 5.
L'idée est d'utiliser la correspondance de Curry-Howard.
En math, on démontre souvent des trucs du genre: A implique B.
En info, on code souvent des fonctions qui prennent A et qui rendent B.
Si on réinterprète les maths, le théorème A implique B, ce n'est rien d'autre qu'une fonction qui, à partir d'une preuve de A, te rend une preuve de B. C'est la même chose.
En brodant un peu (beaucoup), on obtient un truc comme COQ qui permet de générer du code certifié. La seule chose, c'est que le mode de programmation est carrément spécial.
Exemple, pour programmer un tri, on démontre le théorème suivant:
Il existe une fonction f de l'ensemble des listes dans l'ensemble des listes telle que
- f(l) est une permutation de l
- f(l) est triée.
Une fois le théorème démontre, on peut demander à COQ de sortir du code implémentant une fonction qui vérifie les hypothèses du théorème: un tri.
Bref, le jour où les programmeurs de base sauront utiliser ce genre d'outil n'est pas encore arrivé.