Re: Categories for SPARK on Rosetta Code (Was: SPARK : third example for Roesetta - reviewers welcome)

["(see below)" <yaldnif.w@blueyonder.co.uk>]

On 20/08/2010 09:40, in article
3ed38f7f-372d-422e-9bda-eca8a73d3f0d@x21g2000yqa.googlegroups.com, "Phil
Thornley" <phil.jpthornley@gmail.com> wrote:

> On 19 Aug, 07:19, Jacob Sparre Andersen <spa...@nbi.dk> wrote:
>> Dmitry A. Kazakov wrote:
>>> Phil Thornley wrote:
>>>> Dmitry A. Kazakov wrote:
>>>>> I would also suggest Rosetta Maintainers a new category (we should
>>>>> invent a good clear name for it, e.g. "static analysis", "DbC",
>>>>> "provability") to add it to this:
>> 
>>>>> http://rosettacode.org/wiki/Language_Comparison_Table
>> 
>>>> Seem's a good idea - how about "statically analysable".
>> 
>>> It is too vague. In some sense any language is, after all there exist
>>> static analysis tool for C. SPARK is obviously more than that, but it
>>> is tricky to formulate the difference.
>> 
>> Maybe we should simply introduce several categories.
>> 
>> �+ Provable free of exceptions (run-time errors?)
>> �+ Finite memory use.
>> �+ Free of unreachable code.
>> �+ ...?
>> 
>> I'm not quite sure exactly which categories I would formulate. �Maybe
>> somebody from Spark-Team at Praxis can help us with some good
>> suggestions.
> I suspect that if we can't come up with an obvious phrase for what we
> mean then there's no chance of other language users understanding what
> we mean by it and using it correctly.

Proof-oriented?

-- 
Bill Findlay
<surname><forename> chez blueyonder.co.uk