⤓ .md 2026-02-12T055729.000 000000000044256
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)
⤓ .txt 2026-02-12T055729.000 000000000090592
Apache License
Version 2.0, January 2004
http://www.apache.org/licenses/
⤓ .txt 2026-02-12T055729.000 000000000000096
0.1.0-alpha
⤓ .tcl 2026-02-12T055729.000 000000000231208
⤓ .txt 2026-02-19T162221.000 000000000005608
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.