SPARK vs. Ada 2012 for static analysis (Was: Ada 2012 talk at DANSAS'13)

[Jacob Sparre Andersen <jacob@jacob-sparre.dk>]

Paul Rubin wrote:

> Does SPARK-2014 help?  I'm not sure if it exists yet, but I gather
> GNATProve (which is out there) is some kind of precursor to it.

SPARK would of course give compile/analysis-time checking, but we don't
consider it appropriate for the project.  The cost of implementing
sockets and containers in SPARK alone would probably kill that idea.

I'm not sure SPARK-2014 wasn't announced when we started the project,
and I don't consider it ready for real-life use yet, as tasking isn't
covered yet.

We want as much static analysis as we can get, but we are at the same
time working in a context where the value of making an "absolutely
perfect" application isn't that much bigger than writing a "definitely
above average reliability" application.  The whole system also depends
on other parts, which may fail too.  As long as we have a few orders of
magnitude fewer failures than the other parts, we are quite happy.

As I see things, the important place for complete static analysis
(i.e. SPARK) is in components which have a unique possibility of
breaking your system.  One obvious example is a PRNG used for
cryptography; if it is broken, your whole system is broken, and nothing
else can break the system in quite the same way.

Greetings,

Jacob
-- 
»You know the world has gone crazy when the best rapper is a
 white guy, the best golfer is a black guy, the swiss hold
 the America's cup, France is accusing the U.S. of
 arrogance, and Germany doesn't want to go to war«