Microsoft Research dévoile F* : un langage de programmation orienté preuve
F* (prononcé F étoile) est un langage de programmation généraliste orienté preuve, prenant en charge à la fois la programmation purement fonctionnelle et la programmation avec effets de bord. Il combine la puissance expressive des types dépendants avec l'automatisation des preuves basée sur la résolution SMT et la preuve de théorèmes interactive basée sur les tactiques. Les programmes F* se compilent, par défaut, en OCaml. Divers fragments de F* peuvent également être extraits vers F#, C ou Wasm à l'aide de l'outil KaRaMeL, ou vers du code assembleur à l'aide de la chaîne d'outils Vale. F* est implémenté en F* et initialisé à l'aide d'OCaml. F* est open source sur GitHub et est en développement actif par Microsoft Research, Inria et la communauté. Il est utilisé dans plusieurs projets, notamment Mozilla Firefox et le noyau Linux, démontrant son applicabilité à la sécurité, à la cryptographie et au développement de systèmes.