rado
Formality
rado | Formality | |
---|---|---|
1 | 29 | |
0 | 2,014 | |
- | - | |
0.0 | 9.9 | |
over 2 years ago | over 2 years ago | |
Idris | JavaScript | |
- | 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.
rado
-
A dependently typed language for proofs that you can implement in one day
> in practice, what kind of proof are people building when building real world programs ?
Here's an example of a proof from a Turing machine simulator written in Idris [1]. The claim is that the length of the tape never decreases after taking a step.
The "claim" is stated in the type signature, and the "proof" is an implementation of that type. That's what "propositions as types" means. The whole thing looks like a regular function, except that it doesn't do anything and it never gets called. However, by virtue of having been accepted by the type-checker it verifies the claim about that piece of the program's behavior.
[1] https://github.com/nickdrozd/rado/blob/86790bbb218785e57ea88...
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?
PomPom-Language - The cuteness implementation of a dependently typed language.
reach-lang - Reach: The Safest and Smartest DApp Programming Language
elixir-maybe - A simple implementation of the Maybe type in Elixir, intended as an introduction to Functors, Applicative Functors and Monads
apalache - APALACHE: symbolic model checker for TLA+ and Quint
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.
kind - Kubernetes IN Docker - local clusters for testing Kubernetes
monadless - Syntactic sugar for monad composition in Scala
cicada - Cicada Language
anders - 🧊 Модальний гомотопічний верифікатор математики