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