Note the article you're citing is going from Ada (already strong safety checks, but you can still write bugs, just not a whole class of them) to Spark2014, so f

Note the article you're citing is going from Ada (already strong safety checks, but you can still write bugs, just not a whole class of them) to Spark2014, so formal proof of absence of runtime errors (first) and automated verification of functional properties. Even nicer, in a stdlib, so not a toy example and something to build on... You're showing (thanks !) how to go (with some effort, but not so much) from 'so much safer than C already' to 'no bug let's move on and maybe remove all the runtime checks to get C-like performance or better'. I'd say it looks pretty cool.