2023-01-17 15:49:34 +03:00
< div align = "center" >
2022-07-14 05:19:47 +03:00
2023-01-17 15:49:34 +03:00
![banner]
[![crates.io][crates.io-badge]][crates.io]
[![discord.invite][discord.badge]][discord.invite]
![build.badge]
**Kind** is a **pure functional programming language** and **proof assistant** .
[Getting started ](#getting-started ) •
[Examples ](#examples ) •
[Installation ](#installation )
2023-01-17 15:58:25 +03:00
2023-01-17 15:49:34 +03:00
< / div >
# Getting started
2022-07-19 04:47:18 +03:00
2023-09-10 23:45:55 +03:00
It is a complete rewrite of [Kind1 ](https://github.com/HigherOrderCO/Kind-Legacy ), based on
[HVM ](https://github.com/HigherOrderCO/HVM ), a **lazy** , **non-garbage-collected** and **massively parallel** virtual
machine. In [our benchmarks ](https://github.com/HigherOrderCO/Functional-Benchmarks ), its type-checker outperforms every
2022-09-02 19:40:09 +03:00
alternative proof assistant by a far margin, and its programs can offer exponential speedups over Haskell's GHC. Kind2
unleashes the [inherent parallelism of the Lambda
2023-09-10 23:45:55 +03:00
Calculus](https://github.com/VictorTaelin/Interaction-Calculus) to become the ultimate programming language of
2022-09-02 19:40:09 +03:00
the next century.
2022-07-19 04:47:18 +03:00
2023-01-17 15:49:34 +03:00
< div align = "center" > < b > Welcome to the inevitable parallel, functional future of computers! < / b > < / div >
2022-07-19 04:47:18 +03:00
2023-01-17 15:49:34 +03:00
## Examples
2022-07-19 04:47:18 +03:00
2022-09-02 19:40:09 +03:00
Pure functions are defined via equations, as in [Haskell ](https://www.haskell.org/ ):
2022-07-19 04:47:18 +03:00
2022-09-02 19:40:09 +03:00
```javascript
// Applies a function to every element of a list
2023-03-23 14:45:45 +03:00
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)
2022-07-19 04:47:18 +03:00
```
2023-01-15 22:17:01 +03:00
Theorems can be proved inductively, as in [Agda ](https://wiki.portal.chalmers.se/agda/pmwiki.php ) and [Idris ](https://www.idris-lang.org/ ):
2022-09-02 19:40:09 +03:00
```javascript
// Black Friday Theorem. Proof that, for every Nat n: n * 2 / 2 == n.
2023-03-23 14:45:45 +03:00
BlackFridayTheorem (n: Nat) : Equal Nat (Nat.half (Nat.double n)) n
BlackFridayTheorem Nat.zero = Equal.refl
BlackFridayTheorem (Nat.succ n) = Equal.apply (x => Nat.succ x) (BlackFridayTheorem n)
2022-09-02 19:40:09 +03:00
```
2023-05-09 23:30:05 +03:00
For more examples, check the [Kindex ](https://github.com/HigherOrderCO/Kindex ).
2022-07-14 05:19:47 +03:00
2023-01-17 15:49:34 +03:00
# Installation
2022-07-14 05:57:15 +03:00
2022-09-02 19:40:09 +03:00
First, install [Rust ](https://www.rust-lang.org/tools/install ) first, then enter:
2022-07-19 04:47:18 +03:00
```
2023-05-10 00:13:39 +03:00
cargo +nightly install kind2
2022-07-19 04:47:18 +03:00
```
2022-09-02 19:40:09 +03:00
Then, use any of the commands below:
2022-07-14 05:57:15 +03:00
2022-07-23 20:56:54 +03:00
Command | Usage | Note
---------- | ------------------------- | --------------------------------------------------------------
Check | `kind2 check file.kind2` | Checks all definitions.
Eval | `kind2 eval file.kind2` | Runs using the type-checker's evaluator.
Run | `kind2 run file.kind2` | Runs using HVM's evaluator, on Rust-mode.
2023-05-09 23:30:05 +03:00
To-HVM | `kind2 to-hvm file.kind2` | Generates a [.hvm ](https://github.com/higherorderco/hvm ) file. Can then be compiled to a rust crate using HVM.
To-KDL | `kind2 to-kdl file.kind2` | Generates a [.kdl ](https://github.com/higherorderco/kindelia ) file. Can then be deployed to [Kindelia ](https://github.com/higherorderco/kindelia ).
2022-07-19 04:47:18 +03:00
2023-01-17 15:49:34 +03:00
The rust crate can be generated via HVM:
2022-07-19 04:47:18 +03:00
2022-09-02 19:40:09 +03:00
```
2023-01-17 15:49:34 +03:00
kind2 to-hvm file.kind2 > file.hvm
2022-09-02 19:40:09 +03:00
hvm compile file.hvm
```
2022-12-21 03:34:00 +03:00
---
2023-09-10 23:46:27 +03:00
- If you need support related to Kind, email [support.kind@higherorderco.com ](mailto:support.kind@higherorderco.com )
2022-12-21 03:38:01 +03:00
2023-09-10 23:45:55 +03:00
- For Feedbacks, email [kind@higherorderco.com ](mailto:kind@higherorderco.com )
2022-12-21 04:55:30 +03:00
2022-12-21 04:57:44 +03:00
- To ask questions and join our community, check our [Discord Server ](https://discord.gg/kindelia ).
2023-01-17 15:49:34 +03:00
[banner]: ./img/banner.png
[crates.io-badge]: https://img.shields.io/crates/v/kind2?style=flat-square
[crates.io]: https://crates.io/crates/zoxide
[discord.badge]: https://img.shields.io/discord/912426566838013994?style=flat-square
[discord.invite]: https://discord.gg/kindelia
2023-01-17 15:58:25 +03:00
[build.badge]: https://img.shields.io/github/actions/workflow/status/kindelia/kind/ci.yml?style=flat-square