Earlier quoted context omitted.
If you can describe your synthesis operations in terms of some program transformation, you may be able to verify/prove that they preserve certain semantic properties (similar to compiler verification). We have both verified compilers and verified kernels already so this is not a long stretch but it would still be a research project of its own IMO. Also, there has been some research on breaking invariants temporarily…
You can just get it off Libgen as usual: http://dl.acm.org.sci-hub.io/citation.cfm?id=2661142
I did something in this spirit in my Lisp dialect.
I broke the invariant which says "no matter how you terminate a form, the unwind-protect cleanup forms get called".
I broke it by introducing the concept of "absconding": leaving a scope in such a way that the local resources tied to lexical/dynamic contours are left alone. No unwinding calls are done.
The justification is precisely that it is OK if the scope is later re-entered (specifically: restarted via revived continuation). The revived control then finds everything intact --- and can leave the scopes normally at which point the cleanup does take place.
By doing this, I solved the problem of how to integrate continuations with scoped resource acquisition/cleanup, without the horror of dynamic-wind or its ilk.