That’s why you implement it in Ada, and use a SPARK-verified SeedForth-generating backend to emit the “code” — you get all the [verified/provable] consistency from SPARK and let the Forth be the ultra-lowlevel that it is.
That’s why you implement it in Ada, and use a SPARK-verified SeedForth-generating backend to emit the “code” — you get all the [verified/provable] consistency from SPARK and let the Forth be the ultra-lowlevel that it is.