Hacker News Reader

Comment by Havoc | Hacker News Reader

This would have been more credible coming from someone other than the creator of the Go language.

I'm personally leaning into rust for LLM. The whole fussy compiler & errors surface at compile time seems IDEAL for LLMs for me. Hammering compile with tokens is a way better strategy than trying to deduce where stuff may fail at run time and try to catch it via tests.

Tokens are cheap, surprises at runtime are not. So a super anal compiler is what I want. I've looked at lean4 too as the logical next step but not confident I can guide an LLM competently enough for that.

View on HN

fwiw 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.

>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

As someone experimenting with this, it's definitely very difficult to articulate your ideas using advanced type systems. At the same time, the process of doing it often forces me to seriously think through what I want the code to do, which I've noticed qualitatively improves the end result and my understanding of it.

My advice is to be okay with starting small: don't go for full end-to-end correctness or anything like it. Just think of simple properties you want like 'the list returned by this endpoint should always be sorted in ascending order' or 'this operation should be idempotent' and go from there. Use your favorite LLM to help come up with example specifications from natural language, as a starting point, and try hard to fully understand those.

This kind of work does operate at the frontier of what LLMs can do, so expect to run into roadblocks (wasting tokens proving accidentally hard properties, etc).

every time the meta-theory is altered enough by a feature set, feature, or sub-feature that consistency/soundness may be affected the change normally gets wired through the fundamental lemma and the ripple towards it and away from it can be a week of token burn, 10s of millions of tokens across multiple agents - one plan had 28 individual steps, each step of which burned through multiple contexts

this is in comparison to me getting an agent to port Ruby to jart's Cosmopolitan project -- a walk in the park relatively speaking in hindsight

> 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.

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.

Reply on news.ycombinator.com