I'm a small business programmer. I love solving tough problems with Python and PHP. If you like what you're seeing, you should probably follow me here on dev.to and then checkout my blog.
Thanks. The community version of spark had 3 levels of analysis beyond the already insanely capable Ada compiler:
Confirm the code is valid spark (the safe subset of Ada)
Data and flow dependencies (all variables are used, all calculations are effective, etc.)
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!
I'm a small business programmer. I love solving tough problems with Python and PHP. If you like what you're seeing, you should probably follow me here on dev.to and then checkout my blog.
Thanks. The community version of spark had 3 levels of analysis beyond the already insanely capable Ada compiler:
More information here: learn.adacore.com/courses/intro-to...
Yeah formal verification is really neat. Like type-checking on steroids.
At the risk of being argumentative, it's that and so much more.