4 Correctness and limits🔗ℹ

The transformer is conservative about the syntax it changes, reparses the generated text, and leaves unsupported function bodies untouched. It does not evaluate the input, run check-expect tests, compile the program in its active teaching language, or formally prove semantic equivalence. Its equivalence claim is limited to the implemented rewrites and their recognized preconditions.

The generated text can differ in source locations, stack traces, resource use, and timing. Rewrites are not intended to preserve such observations, nor behavior that depends on rebinding or replacing primitive operations. Run the result with the same language and teachpacks as the original, and run the program’s tests before relying on it.