Tous droits réservés

Écrire des programmes prouvés corrects avec Coq

Garantir mathématiquement le respect d'une spécification

Les logiciels occupent une place importante dans les objets technologiques qui nous entourent. Il est parfois impératif qu’un programme ne comporte absolument aucune erreur de programmation. On y parvient en utilisant des techniques permettant de prouver mathématiquement que le programme respecte bien sa spécification, c’est-à-dire qu’il fait ce qu’on attend de lui. Dans cet article, je dirai pour simplifier prouvé correct pour signifier prouvé correct vis-à-vis de sa spécification.1

Dans le présent article, nous montrerons sur un exemple à quoi ressemble l’écriture de programmes prouvés corrects avec l’assistant de preuve Coq. Il s’agit d’un logiciel permettant de faire des démonstrations mathématiques2, qui a la particularité d’intégrer aussi un langage de programmation et qui permet ainsi de mêler programmation et preuves mathématiques. Il n’est pas nécessaire de connaître Coq pour suivre cet article puisque les explications permettent de suivre l’essentiel du propos.

L’exemple que nous développons dans l’article est le cœur d’un mini-compilateur. Les langages source et cible sont délibérément minimalistes pour faciliter les explications. Cet exemple, bien que simpliste, est inspiré par une des applications les plus remarquables de Coq, à savoir un compilateur vérifié pour le langage C, notamment utile pour les applications critiques où l’on veut garantir que la compilation n’introduit pas de bugs.


  1. Il faut alors garder en tête qu’il peut rester des erreurs dans le programme, mais ce seront des erreurs de spécification et non de programmation.
  2. Pour un aperçu de l’utilisation de Coq, voir l’article Un zeste de mathématiques assistées par ordinateur.

Un problème de compilation

Notre objectif est d’écrire un mini-compilateur et de prouver qu’il est correct. Ce compilateur a pour rôle de transformer des programmes écrits dans un langage de programmation source en des programmes écrits dans un langage de programmation cible. Pour prouver qu’il est correct, nous nous assurerons que la signification du programme source est bien la même que celle du programme compilé.

Par souci de simplicité, nous ne donnons pas de définition concrète sous forme de texte aux langages source et cible, ce qui évite de digresser sur l’analyse syntaxique des programmes. Ainsi, il n’y aura pas de code source à proprement parler et les programmes seront directement représentés par des structures de données.

Langage source et langage cible

Pour nos deux langages, un programme est une liste d’instructions, qui manipulent un entier relatif jouant le rôle de compteur. L’exécution de chaque instruction a un certain effet sur le compteur. L’exécution d’un programme consiste à exécuter chaque instruction l’une à la suite des autres, en partant d’un compteur à zéro.

Pour le langage source, les deux seules instructions sont :

  • Add n, qui ajoute l’entier naturel nn au compteur ;
  • Sub n, qui soustraie l’entier naturel nn au compteur.

En utilisant la notation de Coq pour les listes (des crochets pour délimiter la liste et le point-virgule pour séparer les instructions), un programme dans le langage source est par exemple [Add 2; Sub 3; Add 3]. Ce programme termine son exécution avec un compteur à 2.

Le langage cible est plus simple encore, les deux seules instructions sont :

  • Incr, qui ajoute 1 au compteur ;
  • Decr, qui soustraie 1 au compteur.

Un exemple de programme dans le langage cible est [Incr; Incr; Decr; Decr; Incr], qui termine avec un compteur à 1. Un autre exemple de programme est [Decr; Decr; Incr; Decr; Decr], qui termine avec un compteur à -3.

Compilation

Compiler le langage source vers le langage cible, c’est générer un programme dans le langage cible qui a le même comportement qu’un programme donné dans le langage source. Il faut comprendre que la manière de procéder ici est totalement libre, tant que le comportement du programme compilé est le même que celui du programme source.

Nous dirons que le comportement de deux programmes est le même si on aboutit à la même valeur finale pour le compteur. Cette définition est assez simple, mais suffisante pour les besoins de l’article. Notez qu’il existe des définitions plus fines, souvent nécessaires pour les langages de programmation de la vraie vie.

Une manière simple de compiler en ayant bien le même comportement au départ et à l’arrivée, est de traduire directement chaque instruction :

  • l’instruction Add n est transformée en nn fois l’instruction Incr ;
  • l’instruction Sub n est transformée en nn fois l’instruction Decr.

Par exemple, le programme [Add 2; Sub 3] sera compilé en [Incr; Incr; Decr; Decr; Decr]. En exécutant mentalement ces programmes, on voit que le programme source aboutit sur un compteur à -1, tout comme le programme cible et donc que la compilation semble correcte.

On pourrait aussi imaginer un compilateur optimisant, qui ferait des simplifications, pour par exemple compiler [Add 2; Sub 3] directement en [Decr], mais on ne développera pas plus cette idée.

Il faut maintenant effectivement écrire un compilateur pour prouver ensuite qu’il est effectivement correct.

Écriture du cœur du compilateur

Coq nous permet d’écrire le compilateur et de le prouver correct dans un seul outil. Dans cette section, nous commentons des extraits de programme Coq au fur et à mesure, en omettant quelques détails. Le code complet et fonctionnel est listé à la fin de l’article.

Définitions de types pour les langages source et cible

Dans la section précédente, nous avons mentionné que les programmes seront directement représentés par des structures de données, à savoir une liste d’instructions. Coq est un langage fortement typé, nous définissons donc des types pour les instructions, ainsi que des types pour les listes d’instructions.

On commence par définir le langage source. Les quelques lignes ci-dessous définissent d’abord un type instr_s disposant de constructeurs pour chaque instruction de ce langage. Ensuite, on définit une notation (i.e. un raccourci d’écriture) qui dit simplement qu’un programme est une liste d’instructions, ce qui permet d’utiliser les listes définies dans la bibliothèque standard de Coq. Le suffixe _s désignera toujours le langage source dans la suite.

Inductive instr_s :=
  | Add (n:nat)
  | Sub (n:nat).

Notation prog_s := (list instr_s).

On fait de même pour le langage cible. Le suffixe _t désignera le langage cible dans la suite.

Inductive instr_t :=
  | Incr
  | Decr.

Notation prog_t := (list instr_t).

On peut demander d’ailleurs demander à Coq de vérifier le type des exemples de la section précédente. Pour l’exemple de programme source, on entre la commande suivante pour demander à Coq de vérifier le type de l’expression :

Check [Add 2; Sub 3; Add 3].

Coq est un logiciel interactif, il nous répond en redonnant l’expression et son type. (Dans la suite, les réponses de Coq à une commande seront toujours sur fond sombre comme ci-dessous.)

[Add 2; Sub 3; Add 3]
     : prog_s

De même pour l’exemple d’un programme cible, on peut vérifier que Coq déduit le bon type.

Check [Incr; Incr; Decr; Decr; Incr].
[Incr; Incr; Decr; Decr; Incr]
     : prog_t

La fonction de compilation

On a désormais ce qu’il faut pour écrire le compilateur. Il s’agit d’une fonction récursive nommée compile, qui fait appel à la fonction compile_instr pour la compilation d’une instruction individuelle. On applique directement le principe de compilation présenté dans la section précédente.

(* Compilation d'une unique instruction, fonction normale *)
Definition compile_instr (i:instr_s) : prog_t :=
  match i with (* on regarde le type de l'instruction *)
  (* Cas `Add` : on renvoie une liste avec Incr répété n fois *)
  | Add n => repeat Incr n
  (* Cas `Sub` : on renvoie une liste avec Decr répété n fois *)
  | Sub n => repeat Decr n
  end.

(* Compilation d'un programme *)
Fixpoint compile (prog:prog_s) : prog_t :=
  (* On regarde la forme du programme *)
  match prog with
  (* Programme vide, rien à faire *)
  | nil => nil
  (* On compile la première instruction et on met ensuite au bout
     le résultat de la compilation du reste du programme *)
  | i::prog0 => (compile_instr i) ++ (compile prog0)
  end.

On peut tester le bon fonctionnement de la fonction sur un exemple. On utilise Compute pour que Coq calcule la valeur d’une expression.

Compute compile [Add 2; Sub 3].
     = [Incr; Incr; Decr; Decr; Decr]
     : prog_t

La fonction semble fonctionner correctement, mais un exemple ne vaut pas une preuve !

Signification des programmes

Avant de prouver que la fonction de compilation est correcte, il est essentiel de définir ce que signifient nos programmes. Sans ça, il est impossible d’exprimer dans Coq le fait que la fonction de compilation doit conserver la signification des programmes.1

Dans la première section, nous avons dit que l’exécution d’un programme correspond à l’évolution du compteur au fil des instructions. Il faut écrire ça formellement dans Coq.

On définit d’abord une notation counter qui est simplement un synonyme pour le type des entiers relatifs Z.

Notation counter := Z.

Signification d’un programme source ou cible

Maintenant qu’on dispose d’un type compteur, il faut écrire des fonctions qui traduisent les instructions en leur effet sur le compteur.

On a traduit littéralement la signification des instructions telles que décrites dans la première section de cet article. L’exécution d’une instruction consiste à prendre un état, ajouter ou soustraire un entier selon l’instruction puis renvoyer le nouvel état correspondant.

La fonction qui réalise l’exécution d’un programme source est une fonction récursive qui fait appel à une autre fonction pour traiter chaque instruction. On pourrait tout faire dans une seule fonction, mais l’utilisation d’une fonction auxiliaire simplifie légèrement l’écriture de la preuve que nous ferons après.

(* Exécution d'une instruction *)
Definition exec_instr_s (i:instr_s) : counter :=
  (* Analyse de cas sur le type d'instruction *)
  match i with
  (* Première instruction, on ajoute n au compteur *)
  | Add n => Z.of_nat n (* Z.of_nat fait la conversion entre entiers naturels et relatifs *)
  (* Deuxième instruction, on soustraie n au compteur *)
  | Sub n => - Z.of_nat n
  end.

(* Exécution d'un programme *)
Fixpoint exec_s (prog:prog_s) : counter :=
  (* Analyse de cas sur un programme *)
  match prog with
  (* programme vide, le compteur est nul *)
  | nil => 0
  (* on exécute l'instruction, puis le reste du programme *)
  | i::prog0 => exec_instr_s i + exec_s prog0
  end.

On a presque exactement la même chose pour le programme cible.

Definition exec_instr_t (i:instr_t) : counter :=
  match i with
  | Incr => 1
  | Decr => -1
  end.

Fixpoint exec_t (prog:prog_t) : counter :=
  match prog with
  | nil => 0
  | i::prog0 => exec_instr_t i + exec_t prog0
  end.

Test sur des exemples

Encore une fois, on peut prouver des exemples pour tester que ça fait bien ce qui est prévu.

Compute exec_s [Add 2; Sub 3].
     = -1
     : counter
Compute exec_t [Incr; Incr; Decr; Decr; Decr].
     = -1
     : counter

Il n’est pas possible de prouver que les fonctions exec_s et exec_t définies ci-dessus sont mathématiquement correctes. Il s’agit de spécifications ; on définit tout simplement ce que l’on veut que les programmes signifient. Les écrire correctement est donc absolument primordial.

Même avec toute la rigueur de Coq, il peut rester des bugs de spec : ce qui est formellement spécifié n’est pas vraiment ce qu’on voulait signifier initialement. On peut parer ce problème en testant intensivement la spécification avec des techniques habituelles de génie logiciel.


  1. Nous utilisons le mot signification par souci de clarté, mais dans le jargon, on parle de sémantique, qui est synonyme.

Preuve de correction de la compilation

Comme nous l’avons évoqué plusieurs fois dans l’article, prouver que la fonction de compilation est correcte, c’est prouver que le programme source et le programme cible associé ont la même signification.

Dans Coq, nous avons choisi de l’exprimer comme suit :

Theorem compile_correct:
  forall (prog:prog_s), exec_s prog = exec_t (compile prog).

Il faut le comprendre comme suit : « Quelque que soit le programme source, l’exécution de celui-ci aboutit au même compteur que l’exécution du programme issu de sa compilation. » Cela sera vrai pour tous les programmes sources possibles, qui sont en nombre infini, et qu’on ne saurait tester exhaustivement.

Bien que ce soit possible, il n’est pas forcément très lisible de démontrer ce théorème de but en blanc. Il est plus clair de démontrer auparavant des propriétés utiles pour la démonstration du théorème principal. Ces propriétés utiles ne se devinent pas forcément a priori, mais s’identifient au fur et à mesure de la démonstration principale, quand on voit les éléments importants de la démonstration.

Propriétés utiles

La première propriété énonce qu’exécuter deux programmes bout à bout, c’est comme additionner le compteur à la fin de l’exécution du premier avec celui à la fin du deuxième. Son utilité vient du fait que la fonction compile contient l’opérateur ++ pour concaténer deux listes, et que cette propriété permet de transférer cette opération au monde des entiers, c’est-à-dire au domaine de la signification des programmes.

Lemma exec_t_app:
  forall (prog1 prog2:prog_t), exec_t (prog1 ++ prog2) = exec_t prog1 + exec_t prog2.

La deuxième propriété sera vraiment le cœur de la démonstration du théorème de compilation, puisqu’elle met en relation la fonction de compilation, l’exécution d’une instruction source et celle de sa version compilée. Elle énonce qu’une instruction source et le résultat de sa compilation ont bien la même signification.

Lemma compile_instr_correct:
  forall (i:instr_s), exec_instr_s i = exec_t (compile_instr i).

Nous passons les démonstrations de ces propriétés pour commenter en détail celle du théorème principal. Sachez juste qu’à chaque fois, la clé de la preuve repose sur les propriétés des entiers relatifs qui permettent de montrer l’équivalence entre l’exécution des programmes. Le code de cet article est listé à la fin de celui-ci.

Démonstration du théorème de correction

Coq est un prouveur interactif. On construit la preuve au fur et à mesure en saisissant des tactiques auxquelles Coq répond en indiquant les hypothèses courantes, suivies de ce qu’il reste à démontrer.

On énonce le théorème et on démarre la preuve.

Theorem compile_correct:
  forall (prog:prog_s), exec_s prog = exec_t (compile prog).
Proof.

Coq nous répond en disant qu’on a un sous-objectif, l’énoncé du théorème lui-même. Les hypothèses sont au-dessus de la barre (il n’y en a aucune présentement) et ce qu’il faut démontrer est en dessous.

1 subgoal
______________________________________(1/1)
forall prog : prog_s, exec_s prog = exec_t (compile prog)

Une technique habituelle quand on travaille avec des listes est de procéder par récurrence. Dans Coq, on utilise pour cela la tactique induction en lui indiquant sur quel objet on souhaite procéder par récurrence.

induction prog.

Coq remplace alors le sous-objectif actuel par deux sous-objectifs. Cela signifie que pour prouver notre objectif initial, il suffit de prouver deux propriétés, à savoir l’initialisation et la propriété de récurrence. En interne, Coq a gardé en mémoire le lien logique entre ces deux propriétés et le théorème initial et saura reconstruire la preuve complète à la fin.

2 subgoals
______________________________________(1/2)
exec_s [] = exec_t (compile [])
______________________________________(2/2)
exec_s (a :: prog) = exec_t (compile (a :: prog))

La première partie est résolue avec trivial, puisqu’il s’agit de quelque chose que Coq peut simplifier et ensuite constater sans aide.

trivial.

La deuxième partie est plus complexe. Coq nous présente la propriété à prouver. On constate aussi la présence de la propriété IHprog, l’hypothèse de récurrence.

1 subgoal
a : instr_s
prog : prog_s
IHprog : exec_s prog = exec_t (compile prog)
______________________________________(1/1)
exec_s (a :: prog) = exec_t (compile (a :: prog))

Il est possible de simplifier beaucoup, car on a une entrée de la forme a::prog qui correspondra à une seule branche du match dans les différentes fonctions en présence. On effectue cela avec la tactique simpl qui sait faire tout un tas de simplifications :

simpl.

L’objectif devient :

1 subgoal
a : instr_s
prog : prog_s
IHprog : exec_s prog = exec_t (compile prog)
______________________________________(1/1)
exec_instr_s a + exec_s prog = exec_t (compile_instr a ++ compile prog)

On est embêté par la concaténation de listes, mais on peut l’éliminer grâce à la première propriété utile démontrée auparavant. On veut remplacer le terme de la forme exec_t (_ + _) par l’autre membre de l’égalité.

L’expression exec_instr_s a peut également être remplacée grâce à la deuxième propriété.

On effectue ces remplacements en utilisant une tactique de réécriture :

rewrite exec_t_app.
rewrite compile_instr_correct.

On arrive alors à ce stade-là :

1 subgoal
a : instr_s
prog : prog_s
IHprog : exec_s prog = exec_t (compile prog)
______________________________________(1/1)
exec_s prog + exec_t (compile_instr a) = exec_t (compile_instr a) + exec_t (compile prog)

C’est le moment d’utiliser l’hypothèse de récurrence pour se débarrasser de exec_s prog.

rewrite IHprog.

Il suffit alors de prouver :

1 subgoal
a : instr_s
prog : prog_s
IHprog : exec_s prog = exec_t (compile prog)
______________________________________(1/1)
exec_t (compile_instr a) + exec_t (compile prog) = exec_t (compile_instr a) + exec_t (compile prog)

On voit que les deux termes sont égaux, mais Coq n’est pas assez malin pour conclure seul, il faut lui dire. Il existe une tactique nommée reflexivity permettant de prouver un objectif sous forme d’égalité entre deux termes ayant la même forme.

reflexivity.

Coq nous dit alors qu’il ne reste plus rien à prouver.

No more subgoals.

On clôt la preuve.

Qed.

C’est fini. Notre fonction de compilation est désormais prouvée correcte vis-à-vis de sa spécification !


Voilà ! Vous avez désormais un aperçu de comment on écrit des programmes prouvés corrects avec Coq, sous réserve que la spécification elle-même corresponde bien au besoin. Cet exemple est tout simple, mais ce genre de techniques est également utilisé sur des projets de grande envergure. En particulier, le compilateur CompCert est essentiellement écrit et prouvé avec Coq, puis extrait automatiquement vers OCaml et bénéficie ainsi d’un bon niveau de performances et de très bonnes garanties sur sa correction.

Coq n’est pas le seul outil dans le domaine des preuves de programmes. Il existe de nombreux autres outils sur le même créneau, avec des capacités diverses et parfois complémentaires. On peut citer par exemple Isabelle, Frama-C et le greffon WP, Why3 et bien d’autres. On note d’ailleurs l’excellence de la recherche française dans ce domaine puisque Coq et Frama-C en sont issus !

Si l’expression « prouvé correct mathématiquement » donne une impression d’infaillibilité, gardez en tête qu’il reste des maillons faibles dans la réalisation des programmes, tels que de potentiels bugs dans la spécification, dans Coq lui-même, dans le compilateur d’OCaml, voire dans le processeur chargé d’exécuter le programme. L’enjeu est tel que de nombreux chercheurs et ingénieurs travaillent à la réalisation de chaînes qui soient complètement vérifiées d’un bout à l’autre, afin d’avoir les garanties élevées qui sont de plus en plus recherchées pour les applications critiques.

Vous trouverez le code intégral de l’article caché ci-dessous, écrit pour Coq 8.13.

(* Require and Imports *)

Require Import List.
Import ListNotations.

Require Import ZArith.
Open Scope Z_scope.

Require Import Extraction.


(* Source language *)

Inductive instr_s :=
  | Add (n:nat)
  | Sub (n:nat).

Notation prog_s := (list instr_s).


(* Target language *)

Inductive instr_t :=
  | Incr
  | Decr.

Notation prog_t := (list instr_t).


(* Compile *)

Definition compile_instr (i:instr_s) : prog_t :=
  match i with
  | Add n => repeat Incr n
  | Sub n => repeat Decr n
  end.

Fixpoint compile (prog:prog_s) : prog_t :=
  match prog with
  | nil => nil
  | i::prog0 => (compile_instr i) ++ (compile prog0)
  end.

Compute compile [Add 2; Sub 3].


(* Semantics *)

Notation counter := Z.

Definition exec_instr_s (i:instr_s): counter :=
  match i with
  | Add n => Z.of_nat n
  | Sub n => -Z.of_nat n
  end.

Fixpoint exec_s (prog:prog_s) : counter :=
  match prog with
  | nil => 0
  | i::prog0 => exec_instr_s i + exec_s prog0
  end.

Compute exec_s [Add 2; Sub 3].

Definition exec_instr_t (i:instr_t) : counter :=
  match i with
  | Incr => 1
  | Decr => -1
  end.

Fixpoint exec_t (prog:prog_t) : counter :=
  match prog with
  | nil => 0
  | i::prog0 => exec_instr_t i + exec_t prog0
  end.

Compute exec_t [Incr; Incr; Decr; Decr; Decr].


(* Proof of correctness *)

Lemma exec_t_app:
  forall (prog1 prog2:prog_t), exec_t (prog1 ++ prog2) = exec_t prog1 + exec_t prog2.
Proof.
  induction prog1.
  - trivial.
  - intros ; simpl ; destruct a ; rewrite IHprog1 ; ring.
Qed.

Lemma compile_instr_correct:
  forall (i:instr_s), exec_instr_s i = exec_t (compile_instr i).
Proof.
  (* La démonstration ci-dessous fonctionne, mais est un peu brouillon. *)
  destruct i ; induction n ;
  trivial ; simpl in IHn ;  unfold compile_instr ; simpl repeat ;
  unfold exec_t ; fold exec_t ;  rewrite <- IHn ; unfold exec_instr_s ;
  unfold exec_instr_t ; rewrite Nat2Z.inj_succ ; ring.
Qed.

Theorem compile_correct:
  forall (prog:prog_s), exec_s prog = exec_t (compile prog).
Proof.
  induction prog.
  - trivial.
  - simpl.
    rewrite exec_t_app. 
    rewrite compile_instr_correct.
    rewrite IHprog.
    reflexivity.
Qed.

Miniature du tutoriel : le logo de Coq, tel que distribué avec le logiciel.

Ces contenus pourraient vous intéresser

2 commentaires

Je savais que ça se faisait, mais j’en avais toujours une petite idée floue parce que je n’avais jamais eu le courage de me documenter d’avantage et donc de braver le jargon mathématique que l’on trouve dans ces ressources en général. Du coup, merci pour ton article qui m’a permis d’avoir une meilleure idée du fonctionnement concret de tout ça ;)

On pourrait aussi imaginer un compilateur optimisant, qui ferait des simplifications, pour par exemple compiler [Add 2; Sub 3] directement en [Decr], mais on ne développera pas plus cette idée.

Là, je pense qu’on reste toujours dans la sémantique : prouver que l’on reste bien conforme aux specs malgré les optimisations diverses qu’on aurait appliquées.

Mais je me posais la question pour d’autres aspects, notamment ceux qui ne sont pas d’ordre sémantique. Par exemple, si mon langage cible c’est de l’assembleur (ce qui est probable pour un compilateur je pense), je dois non seulement m’assurer que les instructions sont conformes aux specs vis-a-vis du langage source, mais je dois en plus m’assurer de ne pas faire n’importe quoi avec mes instructions assembleur (gérer les bornes de la mémoire, ne pas faire des interruptions interdites, ne pas appeler des mauvais syscall…). Dans ce cas, il faudrait donc que mon code de sortie soit conforme à deux specs : celle de la sémantique du langage source, ainsi que celle de ce qui est possible de faire ou non en assembleur ?

Je peux par exemple imaginer le cas où la sémantique serait respectée pour :

Add 40 Add 2 Print Add 69
add X0, X0, #40 ; Add 40
add X0, X0, #2 ; Add 2
bl Print ; Print
add X0, X0, #69 ; Add 69

; En principe, X0 = 111 à ce stade
; Mais pas de chance : X0 n'est peut-être plus dans le bon état
après le retour de la fonction Print !

Dans ce cas il serait possible avec Coq de prouver non pas sur une mais sur deux specs ? L’une portant sur la sémantique de mon langage source, l’autre portant sur les règles d’utilisation et des conventions de l’asm sous la plateforme en question.

On peut même aller plus loin : peut-on aussi prouver que le programme de sortie n’a pas de memory leaks même si le langage source reste parfaitement silencieux sur la gestion de la mémoire, par exemple ?

Dans ce cas il serait possible avec Coq de prouver non pas sur une mais sur deux specs ? L’une portant sur la sémantique de mon langage source, l’autre portant sur les règles d’utilisation et des conventions de l’asm sous la plateforme en question.

Il te faut une spécification de ton assembleur (et potentiellement un modèle de l’architecture cible selon ce que tu veux faire), mais oui c’est l’idée. Ici @Aabu s’est arrêté au niveau du pseudo assembleur de son modèle mais tu peux continuer plus bas. CompCert est obligé de faire ça par exemple.

On peut même aller plus loin : peut-on aussi prouver que le programme de sortie n’a pas de memory leaks même si le langage source reste parfaitement silencieux sur la gestion de la mémoire, par exemple ?

sgble

Pour ça on entre dans le domaine de la preuve de programmes, ça se fait aussi, c’est une discipline reliée, mais c’est plus tout à fait le même job.

EDIT.

Tiens à nouveau une vidéo reliée au Collège de France. La même idée mais en Agda : https://www.college-de-france.fr/site/xavier-leroy/seminar-2018–11–28–11h30.htm

Connectez-vous pour pouvoir poster un message.
Connexion

Pas encore membre ?

Créez un compte en une minute pour profiter pleinement de toutes les fonctionnalités de Zeste de Savoir. Ici, tout est gratuit et sans publicité.
Créer un compte