Formality
reach-lang
Our great sponsors
Formality | reach-lang | |
---|---|---|
29 | 40 | |
2,014 | 588 | |
- | 0.3% | |
9.9 | 5.2 | |
over 2 years ago | 7 months ago | |
JavaScript | Haskell | |
MIT License | Apache License 2.0 |
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
reach-lang
-
i want to become a block chain developer
Here is a link to their website https://reach.sh/ . Check out their documentation, discord (great community), and they have videos on youtube as well!
-
What is the best crypto programming language and why? Looking for insights from programmers.
I'd highly suggest looking into Reach language (reach.sh). It's a smart contract language based on javascript that has the ability to deploy on ethereum, algorand, and conflux blockchains (i'm sure they will add more at some point). It's a lot simpler to learn than solidity for instance.
-
Smart Contract Tool on Algorand
https://reach.sh there are also sdks available for Java, JavaScript, Python, go
-
Introducing the Beta launch of Pokerand.io, a built-from-scratch Poker Platform for the Algorand Blockchain
Pokerand.io is built from the ground-up using Flutter, a UI software development kit created by Google. The Smart Contract, which handles deposits, withdrawals, authentication, and maintains player balances on-chain, is built using the Reach.sh smart contract platform (https://reach.sh/). The Reach contract will be published as an open-source project on GitHub, along with simple NodeJS programs to manually reproduce Deposits and Withdrawals of tokens.
-
Take this downtime to learn a blockchain programming language.
reach.sh is...
-
Defly: Finding Bugs - The background story of the HumbleSwap relaunch.
When this was first released someone commented "RIP reach" and I assumed the contracts were written with reach.sh
-
why Algorand DeFi is underdeveloped?
The second point is somewhat invalid. Aside from pyteal, which compiles python to teal smart contracts, there is also Reach which is JavaScript to teal.
-
I want to make a small P2E (and Free to Earn) game, I have couple of questions regarding that
If you want a game where there are smart contracts and moves are recorded on the blockchain then either I suggest to wait for Cardano sidechains to itself with smart contract languages which are a bit easier (e.g. https://github.com/reach-sh/reach-lang) or simply develop in Solidity on Milkomeda sidechain with MetaMask.
-
How to deploy your Decentralized Application on 4EVERLAND
In this article, we will cover a tutorial on how to build and deploy your decentralized Application on 4everland. For this case, we will be using react js and 4everland will be used to manage our front-end. The Application will use the Ethereum network and it will be written in Reach, a dApp programming language that is simple to learn and has a Javascript syntax.
-
I’m not going to lie
If you want to look at some examples of smart contracts implemented in a higher level language, there's reach, which is Js based, which compiles to various chain vms including avm. Their GitHub has numerous example smart contracts that I found useful. Their docs & walkthroughs are also good to get you started thinking the right way. You may even consider it for implementation if you're comfortable with JS. It also provides compile time assertions that double check your code for things like "value X should only be visible to participant A" which I found great as a concept.
What are some alternatives?
elixir-maybe - A simple implementation of the Maybe type in Elixir, intended as an introduction to Functors, Applicative Functors and Monads
plutus - The Plutus language implementation and tools
rado - Turing machine in Idris, with some cool types
crypto-fees - Website for comparing total daily fees of various blockchain protocols.
apalache - APALACHE: symbolic model checker for TLA+ and Quint
AlgoSwap - Decentralized Uniswap-like exchange for Algorand Standard Assets. Currently a work-in-progress.
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.
hevm - Dapp, Seth, Hevm, and more
go-algorand - Algorand's official implementation in Go.
FormCoreJS - A minimal pure functional language based on self dependent types.
cardano-ledger-specs - The ledger implementation and specifications of the Cardano blockchain. [Moved to: https://github.com/input-output-hk/cardano-ledger]