Re: [Spark] Arrays of Strings

["Marin David Condic" <mcondic.auntie.spam@acm.org>]

I can agree with Hyman's point to some extent. Trying to eliminate all
possible sources of errors via language design is not going to work and only
succeeds in making the language less useful in solving problems. (Sort of
like trying to teach a pig to dance - it doesn't work and only succeeds in
annoying the pig. :-) There isn't really any substitute for solid design and
rigorous testing if you want a stable, reliable end product. A "safe"
language can lead developers to find ugly, difficult ways around the safety
features in order to get what the designers wanted out of the system.

OTOH, there is some value in something like SPARK wherein one can substitute
formal proof of correctness for formal verification by testing. Verification
can be very time consuming. Some features can make it difficult or
impossible to to test an end product and have a high level of confidence
that the end product will not break. To the extent that the formal proof is
faster and more dependable than formal verification, it gets you a better
product in a less costly way - hence your point about the value of SPARK for
a large percentage of the code and other verification methods for the
smaller percentage.

Its all a balancing act. I believe that the safety features of Ada are a
good thing and hence I agree that SPARK can be a good thing too. But a
desire for absolute safety can end up hamstringing a language and you'll
never get the absolute safety anyway. One would hope that language designers
would keep this in mind and look to the target audience to see what features
are useful as well as what features are safe.

MDC
--
======================================================================
Marin David Condic
I work for: http://www.belcan.com/
My project is: http://www.jsf.mil/

Send Replies To: m c o n d i c @ a c m . o r g

    "Going cold turkey isn't as delicious as it sounds."
        -- H. Simpson
======================================================================

Phil Thornley <phil.thornley@baesystems.com> wrote in message
news:3e966fc9$1@baen1673807.greenlnk.net...
>
> There must be very few SPARK based systems that don't have to include
> some non-SPARK code. (One whole chapter of the SPARK book is about
> interfacing to such code.)
>
> But to argue that this makes languages such as SPARK wholly useless is
> specious.
>
> If I am writing the code for a safety-critical system then all of that
> code has to be brought to the same integrity level. If 99% of that is
> SPARK code then the effort to validate that code is minimised and I am
> quite content to put a lot of manual analysis (per line of code) into
> bringing the remaining 1% up to the same integrity level.
>