F* : un langage de programmation orienté preuve
Original : F*: A general-purpose proof-oriented programming language
Pourquoi c'est important
F* illustre l'adoption industrielle de la vérification formelle dans les logiciels critiques.
F* (F star) est un langage de programmation généraliste orienté preuve, développé en open source par Microsoft Research et Inria. Il combine types dépendants, SMT solving et tactiques interactives, et compile vers OCaml, C, F# ou WebAssembly.
F* est un langage de programmation général qui prend en charge à la fois la programmation purement fonctionnelle et la programmation avec effets. Il intègre des types dépendants expressifs combinés à l'automatisation de preuves via SMT solving et la démonstration interactive de théorèmes par tactiques.
Par défaut, les programmes F* compilent vers OCaml. Des sous-ensembles du langage peuvent aussi être extraits vers F#, C ou WebAssembly via l'outil KaRaMeL, ou vers de l'assembleur grâce à la chaîne Vale. F* est lui-même implémenté en F* et bootstrappé via OCaml.
Le projet est open source sous licence Apache 2.0, co-développé par Microsoft Research, Inria et la communauté. Il est utilisé dans plusieurs projets industriels critiques : la bibliothèque cryptographique HACL* alimente Mozilla Firefox, le noyau Linux, Python et mbedTLS. EverParse, générateur de parseurs binaires issu de F*, est déployé dans Windows Hyper-V pour analyser chaque paquet réseau traversant la plateforme cloud Azure.