Kind2

Kind2 是一种 函数式编程语言 和 证明辅助工具。

它是基于 HVM 的全新编写，HVM 是一个 惰性、非垃圾回收 和 大规模并行 的虚拟机。在我们的基准测试中，其类型检查器在所有替代证明辅助工具中表现最佳，其程序的性能可以比 Haskell 的 GHC 提高指数级。Kind2 通过释放 Lambda 计算的内在并行性，成为下一个世纪终极的编程语言。

欢迎来到计算机不可避免的并行、函数式未来！

示例

纯函数通过等式定义，类似于 Haskell

// Applies a function to every element of a list
map <a> <b> (list: List a) (f: a -> b) : List b
map a b Nil              f = Nil
map a b (Cons head tail) f = Cons (f head) (map tail f)

副作用程序通过 monads 编写，类似于 Rust 和 TypeScript

// Prints the double of every number up to a limit
Main : IO (Result () String) {
  ask limit = IO.prompt "Enter limit:"
  for x in (List.range limit) {
    IO.print "{} * 2 = {}" x (Nat.double x)
  }
  return Ok ()
}

定理可以像在 Agda 和 Idris 中一样进行归纳证明

// Black Friday Theorem. Proof that, for every Nat n: n * 2 / 2 == n.
black_friday_theorem (n: Nat) : Equal Nat (Nat.half (Nat.double n)) n
black_friday_theorem Nat.zero     = Equal.refl
black_friday_theorem (Nat.succ n) = Equal.apply (x => Nat.succ x) (black_friday_theorem n)

更多示例，请查看 Kindex。

用法

首先安装 Rust，然后输入

cargo +nightly install kind2

警告

新版本可能不在 cargo 中，因此您可以通过以下步骤安装 Kind2 的当前版本

1. 安装 Rust Nightly 工具链
2. 克隆仓库
3. cargo安装 --路径crates/kind-cli --强制

然后，使用以下任意命令之一

可以通过HVM生成可执行文件

kind2 to-hvm file.kind2
hvm compile file.hvm
clang -O2 file.c -o file
./file

• 如果您需要与Kind相关的支持，请发送电子邮件至[email protected]

• 对于反馈，请发送电子邮件至[email protected]

• 要提问并加入我们的社区，请查看我们的Discord服务器。