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=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,6d79efdb8dde2c5a X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII Path: g2news1.google.com!news1.google.com!npeer01.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!nx02.iad01.newshosting.com!newshosting.com!198.186.194.249.MISMATCH!transit3.readnews.com!news-out.readnews.com!postnews3.readnews.com!not-for-mail Date: Mon, 16 Aug 2010 19:43:57 -0400 From: "Peter C. Chapin" User-Agent: Mozilla/5.0 (Windows; U; Windows NT 6.1; en-US; rv:1.9.2.8) Gecko/20100802 Lightning/1.0b2 Thunderbird/3.1.2 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: SPARK : third example for Roesetta - reviewers welcome References: <589eea9a-0b14-4ae5-bf62-9abf4b33e7fb@i31g2000yqm.googlegroups.com> <82mxsnuhbq.fsf@stephe-leake.org> <4c69a251$0$2371$4d3efbfe@news.sover.net> In-Reply-To: Content-Type: text/plain; charset=ISO-8859-15 Content-Transfer-Encoding: 8bit Message-ID: <4c69cd5f$0$2375$4d3efbfe@news.sover.net> Organization: SoVerNet (sover.net) NNTP-Posting-Host: 42cc1ba0.news.sover.net X-Trace: DXC=dIRTA_<:FE3jde>A;8:=>0K6_LM2JZB_37AN`KiBGR^3:WUUlR<856?JLOhebnjh`37]l6No81]^5 X-Complaints-To: abuse@sover.net Xref: g2news1.google.com comp.lang.ada:13438 Date: 2010-08-16T19:43:57-04:00 List-Id: On 2010-08-16 18:38, Yannick Duch�ne (Hibou57) wrote: > That's not only about users of Rosetta which would be supposed not > clever enough to understand it, that's about usability any one else (at > least some ones else). You cannot make the assumption that if someone > feel this is somewhat scattered, then this one is just not versed enough > to understand how good it is. I didn't mean to imply that Rosetta users (or Python users) are unintelligent. If my comment came across that way, I apologize. My point was that a person who places a high value in conciseness in programming language design (such as many advocates of dynamic languages) is probably not going to be very impressed with SPARK no matter what you do. Adding an extra rules file (or not) isn't going to matter to such a person. > For the time, unless some news comes in the place, I will end with this > conclusion: SPARK's not a language, that's Praxis's tool. When people ask me what SPARK is about I tell them it's an annotated subset of Ada together with a tool set that can be used for deep static analysis of that annotated language. It seems to me that SPARK is both a language and a tool. Perhaps this gets back to a question Phil raised: does it make sense on Rosetta to differentiate between SPARK and SPARK+proofs? In principle the issue comes up with other languages too. C is not much use without a C compiler (a tool). It is true that you can write a C program in isolation. However, the legality of the program is enforced by a tool. If a SPARK compiler existed as a single program that took SPARK source to object code, it would combine the functionality of, at least, the Examiner and a partial Ada compiler. I suppose it could also contain the functionality of the simplifier as well. Would that make all of that functionality part of the SPARK language? If you created an Ada compiler that split semantic analysis into a separate executable would that make the semantic checks "just a tool?" I suppose to really distinguish between language and tool you need to examine the specification of SPARK. Just as the Ada standard defines the Ada language the SPARK "standard" would define the SPARK language. Any additional features would be added by tools. > By the way, if this is really a Praxis's tool as I suppose now, do I > have to understand there will be always one single implementation of > SPARK and a single provider in this area ? That's an interesting question. Oracle is suing Google over Google's use of Java in Android. I suppose this is the nasty quagmire one gets into whenever one starts using proprietary languages. Thankfully Ada has an international standard so the Ada community can avoid some of that. However, there is no international standard for SPARK. At least not as far as I know. Will it become the Java of the formal methods community? Peter