meta-cedille
Formality
| meta-cedille | Formality | |
|---|---|---|
| 1 | 29 | |
| 55 | 2,014 | |
| - | - | |
| 7.5 | 9.9 | |
| 4 months ago | over 2 years ago | |
| Agda | JavaScript | |
| MIT License | MIT License |
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.
meta-cedille
-
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.
Formality
-
A dependently typed language for proofs that you can implement in one day
Also, my current work is using Kind as a foundation, the purpose of this language is exactly what you have asked for, give a check on https://github.com/uwu-tech/Kind.
-
Kind: A Modern Proof Language
Kind has a "how I learned to stop worrying and love the `Type:Type`" vibe. That doesn't make it invalid as a proof language. It just inverts the priority: instead of consistency being the default and expressivity being opt-in (as in Agda, with the `type-in-type` pragma), it is expressive by default, and consistency is an opt-in. I strongly believe that is the right way. We plan to add opt-in termination (thus consistency) checkers, it is just not an immediate priority, but the language is completely ready for that. About `Type in Type` specifically, keep in mind that there are consistent, interesting type theories that feature `Type in Type`. So it isn't problematic in itself, and removing it seems wrong.
About erasure, you can flag an argument as computationally irrelevant by writing `` instead of `(x: A)`. So, for example, in the [Vector/concat.kind](https://github.com/uwu-tech/Kind/blob/master/base/Vector/con...) file, `A`, `n` and `m` are erased. As such, the length of the vector doesn't affect the runtime. As a good practice, you may also write `f` instead of `f(x)` syntax for erased arguments, but that is optional.
> TL;DR -- I think the language looks nice, and the compile to JS (from what I read of the Formcore source) looks to be well done. Also, the docs that are present are well presented in a non-academic way that I find pretty readable.
Thanks for the kind words. We put a lot of effort on the compilers and, while there is still a lot to improve, I'm confident they're ahead of all the other languages, by far.
- Kind has an universal compiler that targets several back-ends. [...] For example, to generate a QuickSort function in JavaScript, just type kind List.quicksort --js. You may never write code in any other language! Available targets: --js, --scm.
- Kind - A modern proof language
-
Kind-Lang: contributions are welcome!
Kind is a functional, general-purpose programming language featuring theorems and proofs. It has the smallest core, a pretty solid JavaScript and Scheme compiler (seriously, check how clean is the generated kind.js), and a syntax that is a middle ground between Haskell and TypeScript, in an attempt to make it more accessible.
I'm writing CONTRIBUTE.md right now.
- First-class modules with self types
What are some alternatives?
lambdalisp - A Lisp interpreter written in untyped lambda calculus
reach-lang - Reach: The Safest and Smartest DApp Programming Language
Kind - A next-gen functional language
elixir-maybe - A simple implementation of the Maybe type in Elixir, intended as an introduction to Functors, Applicative Functors and Monads
coq - Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
rado - Turing machine in Idris, with some cool types
Kind - A next-gen functional language [Moved to: https://github.com/Kindelia/Kind2]
apalache - APALACHE: symbolic model checker for TLA+ and Quint
write-you-a-haskell - Building a modern functional compiler from first principles. (http://dev.stephendiehl.com/fun/)
plutus - The Plutus language implementation and tools
FormCoreJS - A minimal pure functional language based on self dependent types.
awesome-rust-formalized-reasoning - An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.