alt Hacker Newsfwiw I have a bunch of LLMs writing first Lean code and now Agda code.
My observation. LLMs find reasoning about Agda as difficult as I find reasoning about C code. I've thrown a lot of gnarly C and Ruby code at all sorts of LLMs and they have only gotten more and more impressive as frontier models have gotten stronger. With Agda, they're like "hmm, tricky" whereas for me it's an impenetrable fortress. I've asked them why they find Agda so much more difficult to write (and why they have to iterate and reiterate many many many times until they get to a destination whereas they can one-shot and two-shot C and Ruby and they tell me its the multiple competing constraints. GLM is hilarious, it flat out refuses to write Agda code but it reads it well enough. They all read it well enough. Fable is obviously great at it. And Opus 4.8/5.0 are great (if they stay on track and don't sneakily go their own way) but they're too annoying to talk to. On balance Kimi K3 is the best balance of not annoying, relatively cheap, and strong -- great model all round tbh.
So yeah, interesting I've discovered the limits of their ability coding-ability-wise. None of them are that good at designing/aesthetic judgment/architecting so thankfully they still need me in the loop.
Replies
> My observation. LLMs find reasoning about Agda as difficult as I find reasoning about C code.
A bit funny, because I thought... Hmm, so LLM's find Agda natural?
My point being... It's a matter oh habit. After writing C firmware for more than a decade, I can read C easily. I might have to think of some parts and trace the code. But I can grokk it and hold the thing in my head. With Rust on the other hand, I just don't feel it as well. I am afraid writing C gave me brain damage and restricted the lens I can see the world through.
>fwiw I have a bunch of LLMs writing first Lean code
How do you bridge the mental gap?
The gap between me writing high quality rust do this steps and something being logically sound seems enormous to me
Maybe I'm misunderstanding things but I just can't articulate my ideas in casual lean4. But i can do casual rust spec
A huge amount of it is also the amount of training data. Agda will have little training data so the result will not be nearly as good.
I did a shoot out of making AI make the same simple desktop app from a SwiftUI reference for 30 different language & desktop framework combinations, and by far the best implementation came from the electron web typescript one. The least amount of LoC, the best and most complete implementation and the fastest to implement.