F*
F*
软件描述
F* 是一种类似 ML 的函数式编程语言，旨在实现程序验证。F* 可以表达程序的精确规范，包括功能正确性性质。用 F* 编写的程序可被转换为 OCaml 或 F# 以供执行。
官方网站
访问软件的官方网站了解更多信息
www.fstar-lang.org
安全链接HTTPS
什么是 F*?
F*（读作 F 星）是一种类似 ML 的函数式编程语言，旨在用于程序验证。其类型系统包含多态性、依赖类型、单子效应、精化类型以及最弱前置条件演算。这些特性共同支持对程序进行精确且简洁的规格描述，包括功能正确性属性。F* 的类型检查器通过结合 SMT 求解与手动证明，力求证明程序满足其规格。用 F* 编写的程序可被翻译为 OCaml 或 F# 以供执行。
