Comment by wtetzner

And because of that, we check in the generated code, not the high-level abstraction. So to understand your program, you have to read the output, not the input.