[solomonb]

This is really cool, but why wouldn't you just use a more richly typed target language and skip this process? You could use Liquid Haskell (for refinement types) or Lean (for full dependent types) and be able to put these invariants directly in your program rather then in a sidecar.

[pyrex41]

If you are the kind of person that immediately reaches for this solution -- then I agree, yes you should. You could even do it in Shen! (https://news.ycombinator.com/item?id=39602472, https://news.ycombinator.com/item?id=9297665)

But, for everyone else: even if you skipped the sidecar entirely, didn't use the codegen, you just had the AI interpret the spec'd application into a short Shen proof, iterate until it's internally consistent / compiles...now you have a spec that is internally consistent, straightforward for human to understand, and much stronger context for the LLM than English language spec alone.

[ianhorn]

Not the author, but I've been doing this kind of thing with Lean. I'm still trying to figure out how to make this workflow play nicely with other systems. I have a bunch of rust code that I want these kinds of guarantees on, and that code has third party dependencies that would be terrible to give up. It's totally unclear right now how to get the best of both worlds.

[pyrex41]

I would add, re: Shen -- it's sequent calculus and unique type system (type system itself is Turing complete) give you a lot of flexibility here.

[solomonb]

Shen is one of those projects i've always wanted to dig into a bit but have never found the time sadly.