F*

F*
	File:Fstar-official-logo-2015.png
編程範型	多範式：函數式、指令式、面向對象、元編程、並發編程
設計者	微軟研究院、INRIA
當前版本	Template:Software version
型態系統	靜態類型、強類型、類型推斷
操作系統	Linux, macOS, Windows
許可證	Apache許可證
文件擴展名	.fst
網站	https://fstar-lang.org/
受影響於
	F#、OCaml、Standard ML、Coq、腳本錯誤：沒有「ilh」這個模塊。、腳本錯誤：沒有「ilh」這個模塊。

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上^[1]。

引用[編輯]

package.lua第80行Lua錯誤：module 'Module:Navbar/configuration' not found