Comment by derrak | Hacker News Reader

Comment by derrak | Hacker News Reader

This looks very interesting.

I think the translation from L0 to L1 is going to become more and more important. There have been a lot of discussions here on HN about how natural language specs “aren’t code” and how LLMs provide no formal relationship between their inputs and outputs.

One way to side step this is to have the LLM translate the NL into a formal language and persuade the human that the formal language captures their intent. This reduces the burden because the user only has to look at and understand the formal language spec, rather than all the code produced by the LLM.

Also once a formal spec is obtained, you can do lots of interesting computation on it. Property based testing comes to mind. Or even full-blown verification of the formal spec. Or, LLMs might be good at recognizing ambiguity. An LLM could generate two formal specs, use an SMT solver to find an input where the specs differ, and help the user use this diff to ask clarifying questions and resolve the ambiguity.

One comment I have is that layers L1 and L2 _might_ be reinventing the wheel slightly. Your ensure statements remind me of Dafny or Verus, for instance, which have a lot of tooling behind them.

Indeed, both Verus and Dafny are very close to home here — thanks for the pointer. I did feel at times that I might be reinventing the wheel a bit.

I also thought about pushing more toward Lean and theorem proving instead of a lighter SMT-style direction, but programming and mathematics diverge quickly unless that abstraction boundary is handled carefully. To me, though, that mostly concerns the L1 -> L2 step.

L2 is still the least settled layer and the one I am actively exploring. The idea there is to let relations acquire semantic interpretations: this relation may be realized as a class, an embedding, a parser, etc. Since there is often more than one valid implementation route, I want that choice to be explicit.

And yes, part of the point is exactly to constrain and verify that the end result still matches the original intent at some IR/formal level.

I have been experimenting with this in a calculator/parser example, where the pieces are starting to come together more nicely: https://github.com/ewiger/len/tree/main/examples/advanced/ca...

So I am beginning to think the layering does offer something beyond plain Markdown specs. L1, at least as I currently see it, is intentionally very small: just types and relations, in a logic-oriented style somewhat closer to Prolog — or even SQL — where the world is modeled relationally and constraints are expressed over that. Essentially having more than one targets on L2 level (at the same time in one module) will help to generate both the code and the semantical verification. That's actually a very fruitful observation - big thanks!

> I also thought about pushing more toward Lean and theorem proving instead of a lighter SMT-style direction

I think your intuition here is good. For these settings I think you want formal methods that are highly automated.

Question about your calculator example: is the intended use case that the user would write these L0-L2 files? Or is it expected that an LLM would write them with user intervention? And the go program, how is that obtained from L2? Is that a symbolic transformation or is the LLM doing it?

Apologies if this is written somewhere and my skimming missed it.

Reply on news.ycombinator.com