Voici la présentation de F*. F* est un langage de programmation polyvalent orienté vers la preuve, qui prend en charge à la fois la programmation purement fonctionnelle et la programmation avec effet, et qui combine la puissance d'expression des types dépendants avec l'automatisation de la preuve.F* est un langage de programmation à types dépendants qui vise à jouer plusieurs rôles :
- Un langage de programmation général, qui encourage la programmation fonctionnelle d'ordre supérieur avec des effets, dans la tradition des langages de la famille ML.
- Un compilateur, qui traduit les programmes F* en OCaml ou F#, et même en C ou Wasm, pour exécution.
- Un assistant de preuve, qui permet d'énoncer et de prouver les propriétés des programmes.
- Un moteur de vérification de programmes, exploitant les solveurs SMT pour automatiser partiellement les preuves de programmes.
- Un système de métaprogrammation, supportant la construction programmatique de programmes F* et les procédures d'automatisation des preuves.
Pour atteindre ces objectifs, la conception de F* s'articule autour de quelques éléments clés, décrits ci-dessous. Tout cela n'a peut-être pas de sens pour vous - ce n'est pas grave, vous l'apprendrez au fur et à mesure.
- Un langage central de fonctions totales avec des types dépendants complets, y compris une forme extensionnelle de conversion de type, des types inductifs indexés et des correspondances de motifs, des fonctions récursives avec une vérification sémantique de la terminaison, des types de raffinement dépendants et un sous-typage, ainsi qu'un polymorphisme sur une hiérarchie prédicative d'univers.
- Un système d'effets indexés définis par l'utilisateur, pour modéliser, encapsuler et raisonner statiquement sur diverses formes d'effets informatiques, y compris une notion primitive de récursivité et de divergence générales, ainsi qu'un système ouvert d'effets définis par l'utilisateur, avec des exemples comprenant l'état, les exceptions, la concurrence, les effets algébriques, et plusieurs autres.
- Un encodage intégré d'un fragment classique de la logique de F* dans la logique de premier ordre d'un solveur SMT, permettant à de nombreuses preuves d'être automatiquement déchargées.
- Une réflexion au sein de F* sur la syntaxe et l'état de la preuve de F*, permettant aux programmes Meta-F* de manipuler la syntaxe et les objectifs de preuve de F* et aux utilisateurs de construire des preuves de manière interactive avec des tactiques.
DSLs intégrés dans F*
En pratique, plutôt qu'un langage unique, l'écosystème F* est aussi une collection de langages spécifiques à un domaine (DSL). Une utilisation courante de F* est d'y intégrer des langages de programmation à différents niveaux d'abstraction ou pour des tâches de programmation spécifiques, et de concevoir le langage intégré avec un raisonnement spécifique au domaine, une automatisation des preuves et des backends de compilation. Voici quelques exemples :
- Low*, un DSL peu profond pour la programmation séquentielle avec un modèle de mémoire de type C comprenant une gestion explicite de la mémoire sur la pile et le tas ; une logique Hoare pour la correction partielle basée sur des cadres dynamiques implicites ; et un backend personnalisé (Karamel) pour compiler les programmes Low* en C pour une compilation ultérieure par des compilateurs C disponibles dans le commerce.
- EverParse, une intégration peu profonde d'un DSL (superposé au DSL Low*) de combinateurs d'analyseurs syntaxiques et de sérialiseurs, pour les formats binaires de bas niveau.
- Vale, un DSL profondément intégré pour la programmation structurée dans un langage d'assemblage défini par l'utilisateur, avec une logique Hoare pour une correction totale, et une imprimante pour émettre des programmes vérifiés dans une syntaxe d'assemblage compatible avec divers assembleurs standard.
- Steel, une intégration peu profonde de la concurrence en tant qu'effet dans F*, avec une logique de séparation concurrente extensible pour la correction partielle en tant que logique de programme de base, et l'automatisation de la preuve construite en utilisant une combinaison de tactiques Meta-F*, d'unification d'ordre supérieur et de SMT.
Pour avoir un avant-goût de F*, nous allons nous plonger dans quelques exemples. A ce stade, nous ne nous attendons pas à ce que vous compreniez ces exemples en détail, mais cela devrait vous donner un aperçu de ce qui est possible avec F*.
F* est un langage à typage dépendant
La programmation typée dépendante permet de capturer plus précisément les propriétés et les invariants d'un programme à l'aide de types. Voici un exemple classique : le type vec a n représente un vecteur à n dimensions d'éléments typés a ; ou, plus simplement, une liste de n valeurs chacune de type a. Comme d'autres langages typés de manière dépendante, F* supporte les définitions inductives de types.
| Code : | Sélectionner tout |
1 2 3 | type vec (a:Type) : nat -> Type = | Nil : vec a 0 | Cons : #n:nat -> hd:a -> tl:vec a n -> vec a (n + 1) |
Par exemple, voici une fonction récursive append pour concaténer deux vecteurs. Son type indique que le vecteur résultant a une longueur qui est la somme des longueurs des vecteurs d'entrée.
| Code : | Sélectionner tout |
1 2 3 4 5 | let rec append #a #n #m (v1:vec a n) (v2:vec a m)
: vec a (n + m)
= match v1 with
| Nil -> v2
| Cons hd tl -> Cons hd (append tl v2) |
| Code : | Sélectionner tout |
1 2 3 4 5 | let rec reverse #a #n (v:vec a n)
: vec a n
= match v with
| Nil -> Nil
| Cons hd tl -> append (reverse tl) (Cons hd Nil) |
| Code : | Sélectionner tout |
1 2 3 4 5 | let rec get #a #n (i:nat{i < n}) (v:vec a n)
: a
= let Cons hd tl = v in
if i = 0 then hd
else get (i - 1) tl |
F* supporte la programmation avec effet définie par l'utilisateur
Bien que la programmation fonctionnelle soit au cœur du langage, F* ne se limite pas aux fonctions pures. En fait, F* est un langage complet de Turing. Le fait que cela vaille la peine d'être mentionné peut surprendre les lecteurs ayant une expérience des langages de programmation à usage général tels que C# ou Scala, mais tous les langages typés dépendants ne sont pas complets au sens de Turing, car la non-termination peut rompre la solidité. Cependant, F* supporte les fonctions récursives générales et la non-termination d'une manière sûre, sans compromettre la solidité.
Au-delà de la non-termination, F* supporte un système d'effets de calcul définis par l'utilisateur qui peuvent être utilisés pour modéliser une variété d'idiomes de programmation, y compris des choses comme l'état mutable, les exceptions, la concurrence, les entrées-sorties, etc.
Ci-dessous se trouve du code dans un dialecte F* appelé Low* qui fournit un modèle de programmation séquentiel et impératif de type C avec une mémoire mutable. La fonction malloc_copy_free alloue un tableau dest, copie le contenu d'un tableau d'octets src dans dest, désalloue src et renvoie dest.
| Code : | Sélectionner tout |
1 2 3 4 5 6 7 8 9 10 11 12 13 | let malloc_copy_free (len:uint32 { 0ul < len })
(src:lbuffer len uint8)
: ST (lbuffer len uint8)
(requires fun h ->
live h src /\
freeable src)
(ensures fun h0 dest h1 ->
live h1 dest /\
(forall (j:uint32). j < len ==> get h0 src j == get h1 dest j))
= let dest = malloc 0uy len in
memcpy len 0ul src dest;
free src;
dest |
- La signature de type de la procédure affirme que, sous certaines contraintes imposées à l'appelant, l'exécution de malloc_copy_free est sûre (par exemple, elle ne lit pas en dehors des limites de la mémoire allouée) et qu'elle est correcte (c'est-à-dire qu'elle copie avec succès src dans dest sans modifier d'autre mémoire).
- Étant donné l'implémentation d'une procédure, F* construit en fait une preuve mathématique qu'elle est sûre et correcte par rapport à sa signature.
Bien que d'autres vérificateurs de programmes offrent des fonctionnalités similaires à celles que nous avons utilisées ici, F* se distingue par le fait que la sémantique des programmes avec effets de bord (comme la lecture et l'écriture de la mémoire) est entièrement encodée dans la logique de F* à l'aide d'un système d'effets définis par l'utilisateur.
Alors que malloc_copy_free est programmé dans Low* et spécifié en utilisant un type particulier de logique Floyd-Hoare, il n'y a rien de vraiment spécial à ce sujet dans F*.
Voici, par exemple, un programme concurrent dans un autre dialecte F* défini par l'utilisateur et appelé Steel. Il incrémente deux références allouées au tas en parallèle et est spécifié pour la sécurité et la correction dans la logique de séparation concurrente, un type de logique Floyd-Hoare différent de celui que nous avons utilisé pour malloc_copy_free.
| Code : | Sélectionner tout |
1 2 3 4 | let par_incr (#v0 #v1:erased int) (r0 r1:ref int)
: SteelT _ (pts_to r0 v0 `star` pts_to r1 v1)
(fun _ -> pts_to r0 (v0 + 1) `star` pts_to r1 (v1 + 1))
= par (incr r0) (incr r1) |
Source : Introduction du langage F*
Et vous ?
Quel est votre avis sur le sujet ?Voir aussi :
La version 5.0.0 d'OCaml, le langage de programmation multi-paradigme est disponible, elle apporte le support du parallélisme en mémoire partagée et les gestionnaires d'effets La version 6 de F#, le langage de programmation fonctionnel conçu par Microsoft, est disponible, plus rapide et plus interopérable, elle apporte de nouvelles fonctions Faut-il éviter d'utiliser des classes et s'appuyer autant que possible sur une approche fonctionnelle ? Un point de vue d'Andy Peterson basé sur son expérience en entreprise avec Typescript 
