After months of getting things done w/ Claude Code, I've spent ~5 days programming by hand in Lean and a liquid typed language and it's…SO GREAT? I love living in a world where I can get 1000s of mindless LOC in a minute, but also spend an hour on 10 gorgeous handcrafted lines.
@shriramk I’m doing something very similar. I spent the weekend before last learning Lean by hand and really enjoyed it.
It’s definitely slow going but the two books, Functional Programming in Lean and Theorem Proving in Lean, are really great resources. Clearly written and with lots of examples.
The Lean 4 language itself is amazing. Feels a lot like Haskell but with a much more powerful and better integrated type system.
@mdreid Lean4 is definitely my favorite *programming language* of the many, many proof assistants I've tried (well, ML excluded). It's nice because you can just treat it as a proper language if you want — rather like ML and, even more spectacularly, ACL2.
@edwinb @ohad @mdreid
I think the real win here is "the richer the types, the more we can confine the behavior, so let's focus on nailing down the types and then let the reward-hacking machine run wild filling in the bodies".
OUR MOMENT IS FINALLY HERE! Jut backwards, as Ohad says.
(And separately thinking about the cognitive science needed to make sure we get the types right. But don't tell a functional programmer humans may be involved…)
@shriramk @pigworker has been playing **that** game even longer
@ohad @pigworker @edwinb @mdreid
Yes, and you can go back several more decades. (-:
Oct 12, 2026, 1:00 AM@shriramk Don't wander far. Stick with the handcrafting.
@Nead Waaay too late for that.
@shriramk Or just 1 gorgeous handcrafted line:
https://web.archive.org/web/20070205060623/http://catpad.net/michael/apl/
@shriramk You missed the bit about you helping burn the planet, partaking in the mass theft of the labour of a generation, and helping fascist oligarchs who are recklessly building a financial bubble that has sucked the air out of any business needing compute or memory, and the genocide that is an inevitable consequence of their ideology.
Still happy?