Microsoft Research präsentiert F*: Eine beweisorientierte Programmiersprache
F* (gesprochen F Stern) ist eine allgemeine, beweisorientierte Programmiersprache, die sowohl rein funktionale als auch nebenwirkungsbehaftete Programmierung unterstützt. Sie kombiniert die Ausdruckskraft abhängiger Typen mit der Beweisautomatisierung basierend auf SMT-Solving und taktikbasiertem interaktivem Theorembeweisen. F*-Programme kompilieren standardmäßig nach OCaml. Verschiedene Fragmente von F* können auch mit dem Tool KaRaMeL nach F#, C oder Wasm oder mit der Vale-Toolchain nach Assembler extrahiert werden. F* ist in F* implementiert und wird mit OCaml gebootet. F* ist Open Source auf GitHub und wird aktiv von Microsoft Research, Inria und der Community entwickelt. Es wird in verschiedenen Projekten eingesetzt, darunter Mozilla Firefox und der Linux-Kernel, was seine Anwendbarkeit in den Bereichen Sicherheit, Kryptographie und Systementwicklung zeigt.