ParaSail vs Sparkel vs SPARK

[STEV]

I do not know either of the above languages.

According to the SPARK homepage, the language was "specifically designed for engineering high-reliability applications".

My question is: how does Sparkel compare to SPARK?

Does one language have some safety features that are not included in the other?

And how does ParaSail compare to Sparkel in that respect?

[Tucker Taft]

Sparkel and ParaSail are effectively equivalent semantically, but use a somewhat different surface syntax.  Sparkel follows the Ada model of packages and types within them, while ParaSail uses the interface/class model familiar from Java.  There are actually two more languages in the same family, namely "Parython" and "Javallel" which represent ParaSail in Python's and Java's clothing, respectively.  When I started working on ParaSail I didn't want concerns about  curly braces vs. begin/end vs. indentation-is-significant syntax approaches to derail its consideration as an interesting new way to think about inherently safe, pervasive parallelism.

As far as SPARK vs. Sparkel, SPARK was designed (many years ago) to support formal verification using classic proof technology, and the language was based on Ada, but simplified to make formal proof easier to accomplish.  This meant eliminating pointers (and associated heap allocation), parameter aliasing, and exception handling.  Well it turns out ParaSail and Sparkel emerged with those same simplifications, so in some ways SPARK is a natural springboard for a simplified and safe pervasively parallel language like ParaSail/Sparkel.  Sparkel is mostly upward compatible with SPARK, though not rigidly so.  It has a more dynamic memory model (objects are expandable and shrinkable at run-time), though it does it without having pointers at the user level nor requiring any kind of asynchronous garbage collection.  All memory allocation and deallocation is synchronous with user-visible operations (like creating an object or setting an object to the null value), so its automatic memory management need not introduce complexity or non-determinism into analyzing the real-time behavior of a program.  And of course Sparkel has safe pervasive parallelism.

SPARK is a commercial product, and is undergoing its own evolution, and it will be interesting to see how some of the ideas in ParaSail/Sparkel will feed back into that.  Certainly fine-grained parallelism (reminiscent of ParaSail) is on the agenda for Ada as a whole, and it is likely that that will be incorporated into SPARK soon after it shows up in Ada (or potentially even before).  We are also considering adding a more dynamic memory model into SPARK, somewhat along the lines of that provided by ParaSail/Sparkel, though perhaps using "unique"/"owning" pointers rather than expandable objects, though the net effect is pretty much the same.

Let me know whether the above answers most of your questions!

-Tuck

--
You received this message because you are subscribed to the Google Groups "ParaSail Programming Language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to parasail-programming-language+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[STEV]

Thank you for the quick and informative response.

From what you wrote I conclude that I should learn SPARK (first), since it is a commercial product and therefore probably has a better support / development speed, and since picothreads will probably be incorporated into the language at some point.

--Steve

[Tucker Taft]

Yes, you can't go wrong learning SPARK.  There is a nice new book out about SPARK that has a lot of great examples -- Building High Integrity Applications with SPARK.  Here is the Amazon link to it:

    https://www.amazon.com/Building-High-Integrity-Applications-SPARK/dp/1107656842

Take care,

-Tuck

--
You received this message because you are subscribed to a topic in the Google Groups "ParaSail Programming Language" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/parasail-programming-language/R1nzblzAYqA/unsubscribe.
To unsubscribe from this group and all its topics, send an email to parasail-programming-language+unsub...@googlegroups.com.

For more options, visit https://groups.google.com/d/optout.