Our great sponsors
- Appwrite - The open-source backend cloud platform
- Amplication - open-source Node.js backend code generator
- SurveyJS - A Non-Cloud Alternative to Google Forms that has it all.
- InfluxDB - Collect and Analyze Billions of Data Points in Real Time
- Mergify - Updating dependencies is time-consuming.
|5 days ago||almost 2 years ago|
|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.
CreuSAT: Formally verified SAT solver written in Rust and verified with Creusot
3 projects | news.ycombinator.com | 17 Jun 2022
Unsurprisingly, we can see a growing interest in the Rust ecosystem regarding formal verification. I try to keep https://github.com/newca12/awesome-rust-formalized-reasoning up to date. I will add CreuSAT shortly.
Kani Rust Verifier – a bit-precise model-checker for Rust
7 projects | news.ycombinator.com | 23 Mar 2022
This dispersed progress is the sign of an absence of maturity but the exploration of this space with Rust is very promising : https://github.com/newca12/awesome-rust-formalized-reasoning
A dependently typed language for proofs that you can implement in one day
4 projects | news.ycombinator.com | 1 Oct 2021
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.
Yes! We're 1 file away from supporting a Python (and any other) back-end. For example, [this](https://github.com/uwu-tech/Kind/blob/master/base/Kind/Comp/...) is the simplified JS back-end. If you just copy/paste that file and edit the syntax to Python instead, we'll have a Python back-end. That kind of contribution is always welcome.
Kind-Lang: contributions are welcome!
2 projects | /r/ProgrammingLanguages | 10 Aug 2021
I'm writing CONTRIBUTE.md right now.
My unedited, uncensored thoughts about Ethereum, Cardano, Tezos, formal proofs and functional programming being a gimmick
6 projects | /r/ethereum | 4 Jun 2021
I mean, I could be ignorant about Elixir, but the first thing you do when programming in a language like Kind, Agda, is modeling your problem with types. Everything follows from that. Elixir doesn't even have sum types! It seems like you can't even express very basic concepts like List, Either, Maybe, List, Monad directly. Let alone more sophisticate concepts like subsets, propositional equality, logical negation? I see libs like this which "implement" half-baked, wrong versions of these concepts in contrived ways. Let me know if I'm wrong, but if you can't even translate the first lines of a Kind program in Elixir, I really can't see it as the same thing, at all. Not being elitist! Just saying these are not the same - and that is okay.
What are some alternatives?
reach-lang - Reach: The Safest and Smartest DApp Programming Language
kani - Kani Rust Verifier
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
Kind - A next-gen functional language [Moved to: https://github.com/Kindelia/Kind2]
apalache - APALACHE: symbolic model checker for TLA+
plutus - The Plutus language implementation and tools
cicada - Cicada Language
kind - Kubernetes IN Docker - local clusters for testing Kubernetes
FormCoreJS - A minimal pure functional language based on self dependent types.
minisat - Minisat Haskell bundle
tptp - Parser and pretty printer for the TPTP language