Kind
A modern proof language (by HigherOrderCO)
meta-cedille
Minimalistic dependent type theory with syntactic metaprogramming (by WhatisRT)
| Kind | meta-cedille | |
|---|---|---|
| 4 | 1 | |
| 3,736 | 60 | |
| 0.0% | - | |
| 9.5 | 5.5 | |
| over 1 year ago | almost 2 years ago | |
| Haskell | Agda | |
| MIT License | MIT License |
The number of mentions indicates the total number of mentions that we've tracked plus the number of user suggested alternatives.
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
Kind
Posts with mentions or reviews of Kind.
We have used some of these posts to build our list of alternatives
and similar projects. The last one was on 2023-06-06.
- Kind: A lambda-calculus based pure programming language
-
Can one use lambda calculus as an IR?
Depending on what you mean by practical it already is! https://github.com/HigherOrderCO/Kind HVM was developed to be an efficient backend for the Kind language from the same folks
-
First (1/5) steps with HVM, A massively parallel, optimal functional runtime in Rust
One thing that you can use right now is Kind, a functional language and proof assistant.
-
Brett Slatkin: Why am I building a new functional programming language?
Hey, that's pretty cool! The lang that targets this runtime is https://github.com/HigherOrderCO/Kind
meta-cedille
Posts with mentions or reviews of meta-cedille.
We have used some of these posts to build our list of alternatives
and similar projects. The last one was on 2023-02-28.
-
Any small/simple proof languages?
If you're interested in something that's small, consistent and being able to prove a reasonable amount of things you might be interested in Cedille or my variation of it, Meta-cedille.
What are some alternatives?
When comparing Kind and meta-cedille you can also consider the following projects:
Functional-Benchmarks - Collection of benchmarks of functional programming languages and proof assistants.
lambdalisp - A Lisp interpreter written in untyped lambda calculus
hvmcc
write-you-a-haskell - Building a modern functional compiler from first principles. (http://dev.stephendiehl.com/fun/)
wat-js - Concurrency and Metaprogramming for JS
Formality - A modern proof language [Moved to: https://github.com/kind-lang/Kind]