DEV Community


Discussion on: I'm programming a sumobot with the world's safest programming language

bosepchuk profile image
Blaine Osepchuk Author

Thanks. The community version of spark had 3 levels of analysis beyond the already insanely capable Ada compiler:

  1. Confirm the code is valid spark (the safe subset of Ada)
  2. Data and flow dependencies (all variables are used, all calculations are effective, etc.)
  3. Provers that demonstrate the spark code will never throw a runtime exception or overflow for any inputs (this is what people usually call "formal verification") -- very cool stuff!

More information here:

awwsmm profile image
Andrew (he/him)

Yeah formal verification is really neat. Like type-checking on steroids.

Thread Thread
bosepchuk profile image
Blaine Osepchuk Author • Edited

At the risk of being argumentative, it's that and so much more.