F*: Microsoft Research veröffentlicht beweisorientierte Programmiersprache

F*: A general-purpose proof-oriented programming language

F* ist eine allgemeine, beweisorientierte Programmiersprache, die funktionale und effektvolle Programmierung vereint. Sie kombiniert abhängige Typen mit Beweisautomatisierung durch SMT-Lösen und Taktik-basiertes interaktives Theorembeweisen. F*-Programme kompilieren standardmäßig nach OCaml, können aber auch nach F#, C, Wasm oder Assembly extrahiert werden. Die Sprache wird von Microsoft Research, Inria und der Community aktiv entwickelt. F* findet Anwendung in sicherheitskritischen Projekten wie Project Everest, HACL* und EverParse, die unter anderem in Firefox, dem Linux-Kernel und Windows Hyper-V eingesetzt werden.