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. ▲ 3
    Kind: A lambda-calculus based pure programming language
    story by nico401 · 2023-11-27 · 0 comments
  4. 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
  5. …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
  6. …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
  7. 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
  8. …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
  9. ▲ 68
    Beyond inductive datatypes: exploring Self types
    story by danny00 · 2021-10-30 · 5 comments
  10. ▲ 3
    Getters and Setters in Kind
    story by LangMakers · 2021-10-17 · 4 comments
  11. …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
  12. …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
  13. …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
  14. 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
  15. ▲ 232
    Kind: A Modern Proof Language
    story by danny00 · 2021-08-11 · 111 comments
  16. ▲ 2
    First class modules with self types
    story by LangMakers · 2021-07-29 · 0 comments
  17. 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?
  18. ▲ 2
    Show HN: Kind, a minimal, efficient, practical proof language
    story by LightMachine · 2021-05-16 · 0 comments
  19. …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)
  20. ▲ 2
    Goodbye, JavaScript: Formality is now implemented in itself
    story by LightMachine · 2020-12-15 · 0 comments
  21. 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]
  22. ▲ 3
    Formality Language
    story by VictorTaelin · 2019-12-29 · 0 comments
  23. …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
  24. ▲ 1
    Formality
    story by chaoxu · 2019-09-23 · 0 comments
  25. ▲ 27
    Formality, a (proof)gramming language featuring optimal reductions
    story by LightMachine · 2019-09-10 · 8 comments