ngrislain
Re:Like Terraform, but in Lean 4
on Tuesday September 08, 2026 @01:25PM (#49613455)
Thank you, yes, absolutely, and it's also the perfect language for an AI agents. The more refined the type system, the tighter the feedback loop for the agent.
Like Terraform, but in Lean 4
Re:Ask HN: Advice on Migrating from 1Password?
on Thursday September 03, 2026 @04:53AM (#49547565)
I have been using https://www.passwordstore.org/ for 10 years and am super happy with it.
It does not provide all the convenient integrations of 1Password though.
Language Models Are Anomaly Detectors
LaSuite.coop
Anomaly Detection with LLMs for Cybersecurity
Investigate every security event with an AI agent, without the frontier bill
Vibe Under Constraint
Re:Vibe Under Constraint
on Tuesday June 23, 2026 @03:40PM (#48650255)
Vibe coding is great. You describe what you want, the agent writes it, the tests pass, you ship. It keeps working right up to the moment it does not: the job gets killed by the OOM reaper in production, or it opens ten thousand file descriptors and falls over, or it runs fine on the sample and melts on the real dataset.
Re:If AI writes your code, why use Python?
on Tuesday May 12, 2026 @04:28AM (#48105668)
100%, I’ve been writting: Rust, Haskell and Lean 4 with great success with AI. E.g. https://github.com/typednotes/hale
Mamba-3 and the State Space Model Renaissance
The Signature Method in Machine Learning (an interactive reading note)
Re:Zero-Cost POSIX Compliance: Encoding the Socket State Machine in Le...
on Wednesday March 25, 2026 @06:39AM (#47515563)
Yes the user has to be cooperative somehow.
You could emulate linear/affine types like features with indexed monads though.
Re:Zero-Cost POSIX Compliance: Encoding the Socket State Machine in Le...
on Wednesday March 25, 2026 @04:46AM (#47514863)
You are right, what I wrote is more of a PoC. It's valid for blocking sockets on the happy path.
Re:Zero-Cost POSIX Compliance: Encoding the Socket State Machine in Le...
on Wednesday March 25, 2026 @04:23AM (#47514696)
Fair point! Updated. I’m definitely coming at this more from a Lean 4/formal methods perspective than a POSIX one.
Zero-Cost POSIX Compliance: Encoding the Socket State Machine in Lean's Types
Reading Note: Sequential-Parallel Duality in Prefix Scannable Models
Show HN: Lean-pq a typesafe PostgreSQL connector for lean
https://github.com/typednotes/lean-pq
I’ve been building lean-pq, a PostgreSQL connector for Lean 4.While Lean is primarily known for theorem proving, I believe its dependent-types and formal verification features make it the ideal target for AI Agents to generate provably correct code [0].Lean-pq uses FFI to bind to libpq, but leverages Lean’s type system to move database errors from runtime to compile-time:- Compile-time SQL...
Don't Vibe – Prove
Lean-PQ – Type-safe PostgreSQL bindings for Lean 4 via libpq FFI
How to Die Optimally – A Theory of Consumption When AI Takes Your Job
Re:Lean Advent of Code 2025
on Friday December 12, 2025 @08:34AM (#46243969)
Just finished
Re:Advent of Code 2025
on Tuesday December 02, 2025 @10:56AM (#46122525)
Yes, I'm doing it without AI to learn the language, nonetheless I do think that Lean 4 + AI is a super-powerful combination.
Re:Advent of Code 2025
on Monday December 01, 2025 @09:48AM (#46108085)
Yes, this year I'm going for Lean 4: https://github.com/ngrislain/lean-adventofcode-2025
It's a great language. It's dependent-types / theorem-proving-oriented type-system combined with AI assistants makes it the language of the future IMO.
Re:Advent of Code 2025
on Monday December 01, 2025 @06:11AM (#46106033)
A good opportunity to learn a new programming language: https://news.ycombinator.com/item?id=46105849
Re:Lean Advent of Code 2025
on Monday December 01, 2025 @05:44AM (#46105850)
Advent of Code 2025 in Lean...