F*: SMT解析と依存型を組み合わせた証明指向言語
Judul asli: F*: A general-purpose proof-oriented programming language
Mengapa Ini Penting
高保証ソフトウェア開発の実証事例として、産業界での形式検証普及を示す重要な取り組み。
MicrosoftとInriaが共同開発するオープンソース証明指向プログラミング言語「F*」は、依存型とSMTソルバーを組み合わせ、OCamlやC、WebAssemblyへのコンパイルをサポートする。
F*（エフスター）は、Microsoft ResearchとInriaおよびコミュニティが共同開発する汎用証明指向プログラミング言語。純粋関数型プログラミングとエフェクトを持つプログラミングの両方をサポートし、依存型（dependent types）とSMTソルビングに基づく証明自動化、およびタクティクベースの対話型定理証明を組み合わせている。
デフォルトではOCamlにコンパイルされるほか、KaRaMeL（C/Wasm）、Valeツールチェーン（アセンブリ）、F#への出力にも対応。Apache 2.0ライセンスのもとでGitHubにて公開されている。
産業・学術の双方で実用されており、Project Everestの傘下ではHACL*（高保証暗号ライブラリ）、ValeCrypt、EverCryptなどが開発された。これらのコードはMozilla Firefox、Linuxカーネル、Python、Tezosブロックチェーン、WireGuard VPNなどの本番環境に採用済み。また、EverParseが生成するパーサーはWindows Hyper-VおよびAzureクラウドの全ネットワークパケット処理にも使用されている。