fifth

ColorFORTH to SPARK compiler. **Alpha.**

Compiles ColorFORTH source to verified SPARK/Ada code. Input is the `.fifth` text format—ColorFORTH with colors represented as emoji markers. Output includes contracts verifiable with GNATprove.

- Tcl 8.5+ - GNAT/SPARK (for compiling/verifying output)

Apache License Version 2.0, January 2004 http://www.apache.org/licenses/

0.1.0-alpha

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.