HackerLangs
トップ新着トレンドコメント過去質問紹介求人

ngrislain

no profile record

投稿

Vibe Under Constraint - Claude Code writing Lean 4

ngrislain.github.io
3 ポイント·投稿者 ngrislain·17 日前·1 コメント

Mamba-3 and the State Space Model Renaissance

ngrislain.github.io
1 ポイント·投稿者 ngrislain·3 か月前·0 コメント

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

ngrislain.github.io
1 ポイント·投稿者 ngrislain·3 か月前·0 コメント

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

ngrislain.github.io
34 ポイント·投稿者 ngrislain·4 か月前·23 コメント

Reading Note: Sequential-Parallel Duality in Prefix Scannable Models

ngrislain.github.io
2 ポイント·投稿者 ngrislain·4 か月前·0 コメント

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

github.com
2 ポイント·投稿者 ngrislain·4 か月前·1 コメント

Don't Vibe – Prove

ngrislain.github.io
4 ポイント·投稿者 ngrislain·4 か月前·0 コメント

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

github.com
1 ポイント·投稿者 ngrislain·5 か月前·0 コメント

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

ngrislain.github.io
2 ポイント·投稿者 ngrislain·5 か月前·0 コメント

Lean Advent of Code 2025

github.com
1 ポイント·投稿者 ngrislain·7 か月前·2 コメント

Teaching 3D Geometry with Pyxel

ngrislain.github.io
1 ポイント·投稿者 ngrislain·8 か月前·0 コメント

コメント

ngrislain
·17 日前·議論
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 か月前·議論
100%, I’ve been writting: Rust, Haskell and Lean 4 with great success with AI. E.g. https://github.com/typednotes/hale
ngrislain
·4 か月前·議論
Yes the user has to be cooperative somehow. You could emulate linear/affine types like features with indexed monads though.
ngrislain
·4 か月前·議論
You are right, what I wrote is more of a PoC. It's valid for blocking sockets on the happy path.
ngrislain
·4 か月前·議論
Fair point! Updated. I’m definitely coming at this more from a Lean 4/formal methods perspective than a POSIX one.
ngrislain
·7 か月前·議論
Just finished
ngrislain
·7 か月前·議論
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 か月前·議論
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 か月前·議論
A good opportunity to learn a new programming language: https://news.ycombinator.com/item?id=46105849
ngrislain
·7 か月前·議論
Advent of Code 2025 in Lean...