Hacker News Reader

Comment by kragen | Hacker News Reader

that's exciting news! what does your toy implementation do?

It translates natural language into Isabelle/HOL specifications, and then tries to fill these up to prove things. One can then use Isabelle code generation facilities to extract Scala, OCaml, etc. I think the trick is to have a programmer to guide the whole process, especially decomposition into different modules and abstractions.

Nice. I agree that LLMs will be game-changing for easing the writing of specifications/contracts for verified code; it could become the standard. Interesting that you're using Isabelle/HOL for code generation. I'm working towards auto-formalization of maths using LLM translation to an intermediate language between English and the proof assistant (for which I'm leaning towards Isabelle/HOL) and then a toolbox of techniques (i.e. ATP) for the remaining translation. Formalization is too painful at the moment. It's nearly the same problem as yours. But I'm starting out on simpler problems.

So I'm really interested in the "filling up" part, if you have anything to say about it.

what have you been able to get it to write so far?

(i hope this comment didn't sound skeptical or dismissive)

No worries! The comment was fine, I was simply gone so I couldn't reply.

TBH, I haven't written anything impressive, just toy examples that are formally verified.

I imagine making it practical for larger systems would require a lot more work.

i'm curious to know what you mean by toy examples! are we talking about an assignment statement, an arithmetic expression, finding the maximum of a list, insertion sort, mergesort, a parser for a context-free language, a cooperative multithreading system?

Some simple imperative data structures, including simple operations to add, remove, test membership, etc. with formal guarantees.

that sounds awesome! what does the process of getting to one of those proofs look like? is there a lot of back and forth, or is it mostly autonomous?

Mostly autonomous, with a bit of guidance, but this might be because the training set has examples that are similar enough, making interpolation easy.

fantastic! i hope you decide to share more details; i'd love to hear them

Thanks. It's a toy at the minute, there is nothing super impressive.

Taking this forward would require a lot more work and funding to pay for computation to fine-tune models further.

It's an interesting topic, perhaps good for a startup or a research lab in case one finds a decent monetization stream.

pretty sure you'll be able to monetize writing correct software at scale with an llm

Reply on news.ycombinator.com