Re: SPARK : third example for Roesetta - reviewers welcome

["Peter C. Chapin" <chapinp@acm.org>]

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