Formality Alternatives

Similar projects and alternatives to Formality

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a better Formality alternative or higher similarity.

Suggest an alternative to Formality

Reviews and mentions

Posts with mentions or reviews of Formality. We have used some of these posts to build our list of alternatives and similar projects. The last one was on 2021-08-11.
  • Kind: A Modern Proof Language
    news.ycombinator.com | 2021-08-11
    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.

    news.ycombinator.com | 2021-08-11
    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.
    news.ycombinator.com | 2021-08-11
  • 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.
    reddit.com/r/haskell | 2021-08-10
    Hello! Kind is a functional programming language based on self types that has the smallest core, pretty solid JavaScript and Scheme compilers (seriously, check how clean is the generated kind.js is), and a syntax that is a middle ground between Haskell and TypeScript, in an attempt to make it more accessible. In short, it is a general-purpose, practical functional featuring featuring theorems and proofs. Kind still has a lot to evolve, but, at this point in time, it is one of the most mature proof languages in some aspects. We do research related to optimal evaluators, we explore self types, we build web apps (most are in development, but the performance is stellar), and we're close to have great inter-op with Haskell (one file away), EVM compilers (a linearity-checker away). All in all, I believe Kind is a great addition to the functional programming community. We are a small, mostly self-funded team.
    reddit.com/r/haskell | 2021-08-10
    I'm writing CONTRIBUTE.md right now.
  • First-class modules with self types
    reddit.com/r/haskell | 2021-07-29
  • How to implement first-class modules with self types
  • How to implement first class modules with self types
    reddit.com/r/haskell | 2021-07-29

Stats

Basic Formality repo stats
28
1,978
9.9
1 day ago

moonad/Formality is an open source project licensed under MIT License which is an OSI approved license.

Syncfusion - See why our products are consistently getting 4.6 out of 5 stars by your peers.
Syncfusion Essential Studio for JavaScript is a modern UI control library built from the ground up to be lightweight, responsive, modular, and touch-friendly.
syncfusion.com
Find remote JavaScript jobs at our new job board 99remotejobs.com. There are 13 new remote jobs listed recently.
Are you hiring? Post a new remote job listing for free.