I was thinking that if you had a good enough verified mathematical model of your code using TLA+ or similar you could then use an LLM to generate your code in any language and be confident it is correct. This would be Declarative Programming. Instead of putting in a lot of work writing code that MIGHT do what you intend you put more work into creating the verified model and then the LLM generates code that will do what the model intends.