Microsoft Research、証明指向型プログラミング言語F*を発表
2024-12-25
F*（エフスターと発音）は、純粋関数型プログラミングと副作用のあるプログラミングの両方をサポートする、汎用の証明指向型プログラミング言語です。依存型による表現力の高さに、SMTソルバーとタクティクスベースの対話型定理証明に基づく証明自動化を組み合わせています。F*プログラムは、デフォルトでOCamlにコンパイルされます。KaRaMeLツールを使用してF#、C、Wasmに抽出することも、Valeツールチェーンを使用してアセンブリに抽出することもできます。F*はF*で実装され、OCamlを使用してブートストラップされています。F*はGitHubでオープンソースであり、Microsoft Research、Inria、およびコミュニティによって積極的に開発されています。Mozilla FirefoxやLinuxカーネルなど、さまざまなプロジェクトで使用されており、セキュリティ、暗号化、システム開発における応用を示しています。