From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-0.4 required=5.0 tests=AC_FROM_MANY_DOTS,BAYES_00 autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,463c5796782db6d8 X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2003-04-11 05:16:33 PST Path: archiver1.google.com!news1.google.com!sn-xit-03!sn-xit-01!sn-xit-09!supernews.com!news.maxwell.syr.edu!newsfeed-east.nntpserver.com!nntpserver.com!news-west.rr.com!newsfeed.news2me.com!newsfeed2.earthlink.net!newsfeed.earthlink.net!stamper.news.pas.earthlink.net!stamper.news.atl.earthlink.net!harp.news.atl.earthlink.net!not-for-mail From: "Marin David Condic" Newsgroups: comp.lang.ada Subject: Re: [Spark] Arrays of Strings Date: Fri, 11 Apr 2003 08:05:37 -0400 Organization: MindSpring Enterprises Message-ID: References: <1ec946d1.0304090942.3106b4e4@posting.google.com> <1ec946d1.0304100609.52b0fac0@posting.google.com> <1049986095.779228@master.nyc.kbcfp.com> <3e966fc9$1@baen1673807.greenlnk.net> NNTP-Posting-Host: d1.56.b5.0c X-Server-Date: 11 Apr 2003 12:06:02 GMT X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 5.00.2314.1300 X-MimeOLE: Produced By Microsoft MimeOLE V5.00.2314.1300 Xref: archiver1.google.com comp.lang.ada:36084 Date: 2003-04-11T12:06:02+00:00 List-Id: 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 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. >