Présentation de F*
F* (prononcé F star) est un langage de programmation généraliste orienté preuve, supportant à la fois la programmation fonctionnelle pure et la programmation à effets. Il combine la puissance expressive des types dépendants avec l'automatisation de preuve basée sur la résolution SMT et la preuve de théorème interactive basée sur des tactiques.
Fonctionnement de F*
F* compile, par défaut, en OCaml. Divers fragments de F* peuvent également être extraits en F#, en C ou en Wasm à l'aide d'un outil appelé KaRaMeL, ou en assembleur à l'aide de la chaîne d'outils Vale. F* est implémenté en F* et initialisé à l'aide d'OCaml.
Applications et recherches
F* est utilisé dans plusieurs projets, tant dans des contextes industriels qu'universitaires. Parmi ces projets, on trouve HACL*, une bibliothèque de primitives cryptographiques de haute assurance écrite en F* et extraites en C, ainsi que EverParse, un générateur de parseur pour les formats binaires qui produit du code C extrait de F* formellement prouvé.
Recherche et développement
F* est un sujet actif de recherche, tant dans la communauté des langages de programmation que dans celle des méthodes formelles, ainsi que dans les communautés de sécurité et de systèmes. Des travaux de recherche ont porté sur la conception de F* et de ses DSL, tels que Low* et Steel, ainsi que sur des applications en sécurité et en cryptographie, comme la vérification de programmes à ordre supérieur avec le monade de Dijkstra.
let example = Dijkstra.monadize example_program
