Comment by 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=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.