F*

Website: www.fstar-lang.org

Proiectat de: Microsoft Research and Inria[1]

F* (pronunțat F Star) este un limbaj de programare funcțional inspirat de ML și care vizează verificarea programului.

Sistemul său de tip include tipuri dependente, efecte monadice și tipuri de rafinament.

Aceasta permite exprimarea specificațiilor precise pentru programe, inclusiv corectitudinea funcțională și proprietățile de securitate.

Checker-ul de tip F* își propune să demonstreze că programele își îndeplinesc specificațiile folosind o combinație de rezolvare SMT și dovezi manuale.

Programele scrise în F* pot fi traduse în OCAML, F#și C pentru execuție.

Versiunile anterioare ale F* ar putea fi, de asemenea, traduse în JavaScript.

A fost introdus în 2011 și este în curs de dezvoltare activă pe Github.