Re: The future of Spark . Spark 2014 : a wreckage

["Randy Brukardt" <randy@rrsoftware.com>]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:2bvcgf0jmjcv$.79izri1n5n9r.dlg@40tude.net...
> On Thu, 11 Jul 2013 03:10:51 -0700 (PDT), vincent.diemunsch@gmail.com
> wrote:
>
>> Spark syntax needs to be different from Ada syntax because they 
>> manipulate
>> different things : Ada manipulates types like boolean, integers. Spark
>> annotations manipulates propositions based on abstraction of types (that 
>> I
>> call categories).
>
> Yes this is a crucial point. These are two different languages where one
> (Ada) is a subject of another (SPARK). Statements in these languages 
> should
> be visually distinct.

The problem here is that there is a strong overlap in these annotations. If 
you make them completely distinct, you'll have to write most of them twice 
(especially globals contracts, which you'll want for the optimization/code 
generation benefits, and preconditions and predicates, because they expose 
what otherwise are checks buried in subprogram bodies [where they never can 
be eliminated] to the compiler [which can then eliminate them from the call 
site - no matter whether you are using proofs or not]). These to me are a 
code quality issue, and items intended for the Ada compiler have to be in 
the Ada syntax.) And I agree that you don't want to make them completely the 
same either (Ada has no use for the "depends" annotation that I can see; Ada 
code shouldn't have items in it that are of no use to an Ada compiler).

Which leaves us with a problem that isn't obvious to solve. AdaCore is 
trying.

Anyway, I've said enough on this topic.

                                Randy.