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

[Shark8 <onewingedshark@gmail.com>]

On Thursday, August 15, 2013 7:02:17 AM UTC-6, Jacob Sparre Andersen wrote:
> 
> 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.

I see what you're saying, but I [somewhat] disagree: the scope you're using is too small. it's the small "everybody uses it and assumes it's correct" things that need SPARK-verification.

Take DNS for example: there's a *lot* of bugs that have been found in any main DNS0server over the past decade [or two]. Everybody using the internet is interacting with a DNS, even if indirectly. And so it behooves us to eliminate everything [bug-wise] that we can -- which is what formal verification does, and it's what the twp guys who developed Ironsides did. ( http://ironsides.martincarlisle.com/ )

The two papers linked just above the "Download" heading are quite informative and say things much better than I can.

I would love to see a formally-verified OS, and to be honest MS would have a much better product to sell if they did so to their OS instead of worrying about "looking stylish". (See the Windows 8 disaster)