cardano-ledger-specs VS Formality

Integrates with the ledger, consensus and network components that power the Cardano network. (These are also written in Haskell, and we work closely with these teams.)

I'm not a big Cardano fanboy but this doesn't appear to be the case https://github.com/input-output-hk/cardano-ledger-specs/commits/master

Another thing I should mention is that, if you look at the Cardano smart contract integration formal specification, it actually contemplates the potential co-existence of multiple smart contract scripting languages, of which Plutus V1 is merely the first one.

32 bytes long

https://github.com/input-output-hk/cardano-ledger-specs/blob/master/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/API/Wallet.hs#L70

This is the repository with the ledger specifications: https://github.com/input-output-hk/cardano-ledger-specs

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 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 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.