Formality
PomPom-Language
| Formality | PomPom-Language | |
|---|---|---|
| 29 | 8 | |
| 2,014 | 186 | |
| - | - | |
| 9.9 | 0.0 | |
| over 2 years ago | over 1 year ago | |
| JavaScript | Haskell | |
| 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.
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
PomPom-Language
-
I find the often ML-inspired syntax too high of a bar for most programmers to clear when being introduced to a language.
No, I mean this
-
Hacker News top posts: Oct 2, 2021
A dependently typed language for proofs that you can implement in one day\ (39 comments)
- Dependently typed language implementation that is small and easy to follow
- A dependently typed language for proofs that you can implement in one day
- PomPom-Language: A dependently typed language for proofs that you can implement in one day
What are some alternatives?
reach-lang - Reach: The Safest and Smartest DApp Programming Language
WebGoat - WebGoat is a deliberately insecure application
elixir-maybe - A simple implementation of the Maybe type in Elixir, intended as an introduction to Functors, Applicative Functors and Monads
rado - Turing machine in Idris, with some cool types
apalache - APALACHE: symbolic model checker for TLA+ and Quint
Lightning-Network - List of Lightning Network technical issues, bugs, flaws, and exploits.
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