Open Questions (alpha stage)
How does the compiler infer stack effects for user-defined words? The Pre contract generation implies static analysis of stack depth across word compositions. This is non-trivial for recursive or conditionally-branching definitions.
What happens with @ and ! (memory operations)? SPARK verification of unconstrained memory access is a hard problem. The generated Stack_Array is bounded (256 cells), but arbitrary memory operations could challenge provability.
Error handling and diagnostics — no mention of compiler error messages, source location tracking, or diagnostic output.
Testing — no test suite mentioned, though the examples serve as implicit smoke tests.