F*（讀作「F star」）是一個由微軟研究院和INRIA主導開發的、基於ML的依賴類型函數式程序語言，主要用於程序的形式化驗證。
F*的類型系統十分豐富，支持依賴類型、單子化效用（monadic effects）和細化類型（refinement types）。這使其能夠準確地用於表述程序的形式化規範，包括功能正確性和安全性。 F*的類型檢查器通過檢查手寫的證明和SMT自動求解來確保程序符合規範。
使用F*書寫的程序可被編譯到OCaml、F#或C加以執行。早期版本的F*亦支持編譯到JavaScript。
F*語言本身使用F*和F#實現，並可從OCaml或F#引導。它的源碼使用Apache協議授權，目前託管在GitHub上[2]。
引用
外部連結
Wikiwand in your browser!
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.
