F*
F*
软件描述
F* 是一种类似 ML 的函数式编程语言，旨在实现程序验证。F* 可以表达程序的精确规范，包括功能正确性性质。用 F* 编写的程序可被转换为 OCaml 或 F# 以供执行。
官方网站
访问软件的官方网站了解更多信息
官方认证
www.fstar-lang.org
安全链接HTTPS
什么是 F*?
F*（读作 F 星）是一种类似 ML 的函数式编程语言，旨在用于程序验证。其类型系统包含多态性、依赖类型、单子效应、精化类型以及最弱前置条件演算。这些特性共同支持对程序进行精确且简洁的规格描述，包括功能正确性属性。F* 的类型检查器通过结合 SMT 求解与手动证明，力求证明程序满足其规格。用 F* 编写的程序可被翻译为 OCaml 或 F# 以供执行。
主要功能
🔄 替代方案
6 个选择
F# (programming language)
F# 是一种简洁、富有表现力且高效的 .NET 功能性与面向对象语言，可帮助您编写简单的代码来解决复杂问题。
OCaml
OCaml 是一种工业级编程语言，支持函数式、命令式和面向对象的编程风格。
Rocq Prover
一个可信的、工业级的交互式定理证明器及依赖类型编程语言，用于数学、计算机科学等领域的机械化推理。
Isabelle
Isabelle 是一个用于通过计算机编写和检查数学证明的证明助手。
Agda
Agda 是一种依赖类型函数式编程语言。它具有归纳族，即依赖于值的数据类型，例如指定长度的向量类型。它还支持参数化模块、混合运算符、Unicode 字符以及交互式 Emacs...