HackerLangs
TopNewTrendsCommentsPastAskShowJobs

ngrislain

no profile record

Submissions

Vibe Under Constraint - Claude Code writing Lean 4

ngrislain.github.io
3 points·by ngrislain·17 дней назад·1 comments

Mamba-3 and the State Space Model Renaissance

ngrislain.github.io
1 points·by ngrislain·3 месяца назад·0 comments

The Signature Method in Machine Learning (an interactive reading note)

ngrislain.github.io
1 points·by ngrislain·3 месяца назад·0 comments

Zero-Cost POSIX Compliance: Encoding the Socket State Machine in Lean's Types

ngrislain.github.io
34 points·by ngrislain·4 месяца назад·23 comments

Reading Note: Sequential-Parallel Duality in Prefix Scannable Models

ngrislain.github.io
2 points·by ngrislain·4 месяца назад·0 comments

Show HN: Lean-pq a typesafe PostgreSQL connector for lean

github.com
2 points·by ngrislain·4 месяца назад·1 comments

Don't Vibe – Prove

ngrislain.github.io
4 points·by ngrislain·4 месяца назад·0 comments

Lean-PQ – Type-safe PostgreSQL bindings for Lean 4 via libpq FFI

github.com
1 points·by ngrislain·5 месяцев назад·0 comments

How to Die Optimally – A Theory of Consumption When AI Takes Your Job

ngrislain.github.io
2 points·by ngrislain·5 месяцев назад·0 comments

Lean Advent of Code 2025

github.com
1 points·by ngrislain·7 месяцев назад·2 comments

Teaching 3D Geometry with Pyxel

ngrislain.github.io
1 points·by ngrislain·8 месяцев назад·0 comments

comments

ngrislain
·17 дней назад·discuss
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.
ngrislain
·2 месяца назад·discuss
100%, I’ve been writting: Rust, Haskell and Lean 4 with great success with AI. E.g. https://github.com/typednotes/hale
ngrislain
·4 месяца назад·discuss
Yes the user has to be cooperative somehow. You could emulate linear/affine types like features with indexed monads though.
ngrislain
·4 месяца назад·discuss
You are right, what I wrote is more of a PoC. It's valid for blocking sockets on the happy path.
ngrislain
·4 месяца назад·discuss
Fair point! Updated. I’m definitely coming at this more from a Lean 4/formal methods perspective than a POSIX one.
ngrislain
·7 месяцев назад·discuss
Just finished
ngrislain
·7 месяцев назад·discuss
Yes, I'm doing it without AI to learn the language, nonetheless I do think that Lean 4 + AI is a super-powerful combination.
ngrislain
·7 месяцев назад·discuss
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.
ngrislain
·7 месяцев назад·discuss
A good opportunity to learn a new programming language: https://news.ycombinator.com/item?id=46105849
ngrislain
·7 месяцев назад·discuss
Advent of Code 2025 in Lean...