I just finished waiting almost four hours for Fable to write 700 lines of code, based on my three paragraph prompt. Some speed on these harder tasks would definitely be welcome!

It also spent almost 800k tokens on these lines…

I'm very curios what the code is doing.

It is a normalisation procedure for inductive and coinductive data types.

Basically, the code is a function which takes in an expression where you can use generic data structures as variables and then some specific data structures, and it plugs them in for the variables. It then computes the structure of the resulting data type.

So, admittedly not a trivial task – hence the choice of Fable as the model. Also, this would have taken me few days to do by hand! So, we are living in the future! But one could always wish for more speed and more intelligence.

What language?

Agda. Fable and Opus both know it quite well now. They need some guidance to create good-looking code, but man, they know how to grind!