Hacker GitHub

← All repos

HigherOrderCO/Kind

View on GitHub ↗ ★ 3,764 Haskell

A modern proof language

25 mentions on Hacker News by 15 people: 10 stories, 15 comments · first 2019-09-10 · latest 2026-09-18

Mentions per year 25 mentions · busiest year 2021 (12)
20082026
AllStoriesComments NewestTopOldest
  1. …tps://github.com/VictorTaelin/Cedille-Core I also implemented Kind-Lang 5 years ago, way before LLMs: https://github.com/higherorderco/kind I dropped out of Federal University of Rio de Janeiro to study this subject independently, because…
    comment by LightMachine · 2026-09-18 · in Bend 2 and the Vibe-Coding Trap
  2. …[7] https://higherorderco.com [8] https://github.com/HigherOrderCO/bend [9] https://github.com/HigherOrderCO/kind
    comment by 4ad · 2024-12-19 · in Borrow Checking, RC, GC, and Eleven Other Memory Safety Approaches
  3. Hey, that's pretty cool! The lang that targets this runtime is https://github.com/HigherOrderCO/Kind
    comment by nextaccountic · 2023-03-05 · in Building a new functional programming language
  4. …to its ir/bytecode. [1]: https://idris2.readthedocs.io/en/latest/implementation/overv... [2]: https://github.com/Kindelia/Kind https://github.com/VictorTaelin/Elementary-Affine-Type-Theor...
    comment by rq1 · 2022-03-10 · in Fornjot: A next-generation Code-CAD application
  5. …agree about the Blub Paradox, but there's definitely value in Self Types. See, for example, [Kind]( https://github.com/Kindelia/Kind ), which is able to type recursive data types by using Self Types.
    comment by smaddox · 2022-02-16 · in Type Checking as Calculation
  6. Don't forget Kind ( https://github.com/Kindelia/Kind ) which is mentioned in the "How can I Help?" section as a potential language for targeting HVM.
    comment by sixbrx · 2022-02-05 · in High-order Virtual Machine (HVM): Massively parallel, optimal functional runtime
  7. …unsound expressions (for example that don’t terminate), but to have consistency checkers. See: https://github.com/kind-lang/Kind/blob/master/CONTRIBUTE.md#...
    comment by skybrian · 2021-10-30 · in Beyond inductive datatypes: exploring Self types
  8. …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 .
    comment by caotic123 · 2021-10-02 · in Show HN: Dependently typed language for proofs that you can implement in one day
  9. …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…
    comment by LangMakers · 2021-08-11 · in Kind: A Modern Proof Language
  10. …is still a lot to improve, I'm confident they're ahead of all the similar languages, by far. [1] https://github.com/uwu-tech/Kind/blob/master/base/Vector/con...
    comment by LangMakers · 2021-08-11 · in Kind: A Modern Proof Language
  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…
    comment by LangMakers · 2021-08-11 · in Kind: A Modern Proof Language
  12. 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.
    comment by LightMachine · 2021-05-26 · in How inevitable is the concept of numbers?
  13. …being somewhat isomorphic with other interesting correctness/performance/ergonomics problems. [1]: https://github.com/moonad/Formality
    comment by wwright · 2021-01-06 · in Lunar Programming Language (2018)
  14. I wonder if I should take those opportunities to talk about Formality ( https://github.com/moonad/formality ).
    comment by LightMachine · 2020-01-15 · in Patch Critical Cryptographic Vulnerability in Microsoft Windows [pdf]
  15. …almost similar efforts [0] [1] then I found your post [2]. You may be interested also in [3]. [0] https://github.com/moonad/Formality [1] http://imar.ro/~mbuliga/chemlambda-v2.html [2] https://www.reddit.com/r/haskell/comments/dih8xu/optima…
    comment by xorand · 2019-10-21 · in Show HN: Eole, a Lévy-optimal lambda calculus evaluator written in Rust