Kind

The plan for Kind itself seems to be to allow possibly unsound expressions (for example that don’t terminate), but to have consistency checkers. See: https://github.com/kind-lang/Kind/blob/master/CONTRIBUTE.md#...

Also, my current work/job 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.

Thanks for the compliment on FmcToJS! It is probably the most messy part of the whole project though. We can't wait to port it entirely to [JavaScript.kind](https://github.com/uwu-tech/Kind/blob/master/base/Kind/Comp/...). That said, we put a lot of work on it and hell it does produce some satisfying JavaScript code. I'm not familiar with that mechanism, do you have a link? The dependent function type, `∀ (x : A) -> B(x)` allows the type returned by a function call, `f(x)`, to depend on the value of the argument, `x`. The self-dependent function type, `∀ f(x : A) -> B(f,x)` allows the type returned by a function call, `f(x)`, to also depend on the value of the function, `f`. That is sufficient to encode all the inductive datatypes and proofs present in traditional proof languages, as well as many other things.

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. It is still not implemented, 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 it. So it isn't problematic in itself, and removing it seems wrong. About erasure, you can flag an argument as computationally irrelevant by writing `<x: A>` instead of `(x: A)`. So, for example, in the `Vector.concat.kind` [1] file, `A`, `n` and `m` are erased. As such, the length of the

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.

Well [Kind](https://github.com/uwu-tech/kind) has only one "axiom" (the lambda), so, I don't know? This is a really inspiring thought and I'm glad people are debating it for the content and not attacking Wolfram just because.

In defense, I would argue that many modern language design advancements DO relate to multithreading in some way. Rust’s borrow checker and linear/affine types can help with thread safety; OCaml is using algebraic effects to implement multi core behavior; GPU-related experiments (such as Formality [1]) are all about enabling more scalable and reliable parallelism. That said, I don’t think that multithreading is the only interesting or worthwhile part of programming language theory these days. However, I think it is extremely fertile for innovation while also being somewhat isomorphic with other interesting correctness/performance/ergonomics problems. [1]: https://github.com/moonad/Formality