| 1. | | Kernel accepts wrong-structure projections, allowing axiom-free proof of False (github.com/leanprover) |
| 5 points by gopiandcode 51 days ago | past |
|
| 2. | | Using LLM-Based Verification to Eliminate Bugs in Linux's Network Stack (basis.ai) |
| 4 points by gopiandcode 59 days ago | past |
|
| 3. | | Pact: Trustworthy Coordination for Multi-Agentic Ecosystems (basis.ai) |
| 3 points by gopiandcode 4 months ago | past |
|
| 4. | | Building an Unverified Compiler with Agents (basis.ai) |
| 2 points by gopiandcode 5 months ago | past |
|
| 5. | | Lean proved this program was correct; then I found a bug (kirancodes.me) |
| 7 points by gopiandcode 5 months ago | past |
|
| 6. | | Buffer Overflow in Lean_io_prim_handle_read (github.com/leanprover) |
| 2 points by gopiandcode 5 months ago | past | 1 comment |
|
| 7. | | Multi-Agentic Software Development Is a Distributed Systems Problem (kirancodes.me) |
| 1 point by gopiandcode 5 months ago | past |
|
| 8. | | Vibe-Coding a Verified Compiler (JS-2-WASM) (docs.google.com) |
| 3 points by gopiandcode 6 months ago | past | 1 comment |
|
| 9. | | Humanity is stained by C and no LLM can rewrite it in Rust (kirancodes.me) |
| 3 points by gopiandcode 10 months ago | past | 9 comments |
|
| 10. | | Why Lean 4 replaced OCaml as my Primary Language (kirancodes.me) |
| 27 points by gopiandcode on Aug 14, 2025 | past | 5 comments |
|
| 11. | | LLMs pose an interesting problem for DSL designers (kirancodes.me) |
| 220 points by gopiandcode on June 17, 2025 | past | 151 comments |
|
| 12. | | The looming problem of slow and brittle proofs in SMT verification (kirancodes.me) |
| 4 points by gopiandcode on June 8, 2025 | past |
|
| 13. | | How to (actually) prove it – New Frontiers of Mathematics and Computing in Lean (kirancodes.me) |
| 81 points by gopiandcode on May 9, 2025 | past | 17 comments |
|
| 14. | | Functional vs. Data-Driven Development: A Case-Study in Clojure and OCaml (kirancodes.me) |
| 6 points by gopiandcode on March 8, 2025 | past | 1 comment |
|
| 15. | | LeanSSR: An SSReflect-Like Tactic Language for Lean (github.com/verse-lab) |
| 2 points by gopiandcode on March 25, 2024 | past |
|
| 16. | | Sisyphus – Mostly Automated Proof Repair for Verified Libraries (verse-lab.github.io) |
| 2 points by gopiandcode on July 24, 2023 | past |
|
| 17. | | Rhombus in the Rough: A 2D RPG implemented in the Rhombus Racket Lisp dialect (github.com/gopiandcode) |
| 2 points by gopiandcode on May 25, 2023 | past |
|
| 18. | | Petrol: Embedding a type-safe SQL API in OCaml using GADTs (gopiandcode.uk) |
| 3 points by gopiandcode on April 24, 2023 | past |
|
| 19. | | I Wrote an Activitypub Server in OCaml: Lessons Learnt, Weekends Lost (gopiandcode.uk) |
| 154 points by gopiandcode on April 23, 2023 | past | 108 comments |
|
| 20. | | LLaMA-based Emacs Search plugin (reddit.com) |
| 2 points by gopiandcode on March 26, 2023 | past |
|
| 21. | | Show HN: A web front end for your Org-files (codeberg.org/gopiandcode) |
| 92 points by gopiandcode on Dec 2, 2022 | past | 13 comments |
|
| 22. | | Unifying fold left and fold right in Prolog (gopiandcode.uk) |
| 90 points by gopiandcode on Aug 26, 2022 | past | 15 comments |
|
| 23. | | Racket-Rhombus: To Sexp or Not to Sexp? (gopiandcode.uk) |
| 2 points by gopiandcode on Aug 25, 2022 | past |
|
| 24. | | Goodbye C developers: The future of programming with certified program synthesis (gopiandcode.uk) |
| 5 points by gopiandcode on July 5, 2021 | past | 2 comments |
|
| 25. | | Testing Out Algebraic Effects in OCaml for Game Animations (gopiandcode.uk) |
| 3 points by gopiandcode on Jan 2, 2021 | past |
|
| 26. | | Bloom filters debunked: Dispelling 30 Years of bad math with Coq (gopiandcode.uk) |
| 472 points by gopiandcode on July 25, 2020 | past | 126 comments |
|
| 27. | | Structural OCaml Editing in Emacs (ocaml.org) |
| 138 points by gopiandcode on March 14, 2020 | past | 9 comments |
|
