Viewing profile — ngrislain

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…

100%, I’ve been writting: Rust, Haskell and Lean 4 with great success with AI. E.g. https://github.com/typednotes/hale

Yes the user has to be cooperative somehow. You could emulate linear/affine types like features with indexed monads though.

You are right, what I wrote is more of a PoC. It's valid for blocking sockets on the happy path.

Fair point! Updated. I’m definitely coming at this more from a Lean 4/formal methods perspective than a POSIX one.

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 mak…

Just finished

Yes, I'm doing it without AI to learn the language, nonetheless I do think that Lean 4 + AI is a super-powerful combination.

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…

A good opportunity to learn a new programming language: https://news.ycombinator.com/item?id=46105849

Advent of Code 2025 in Lean...