Re: SPARK : third example for Roesetta - reviewers welcome

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Mon, 16 Aug 2010 00:09:17 +0200, Jeffrey Carter  
<spam.jrcarter.not@spam.not.acm.org> a écrit:
> The large number of Check annotations seems to my untrained eye an  
> unusual way to use SPARK. As a comparison, the Tokeneer "core" code is  
> 34769 LOC and contains 27 Check annotations, a much lower ratio of  
> Check/LOC. Is this a good way to present SPARK on Rosetta?
There is no Magic here, what you do not have in Check annotations, you  
hide it in user rules. The reason why I do not like it, is because you do  
not see the proofs any more (or great part of it are missing), this is not  
any more part of the source. Proofs should come with the implementation. I  
cannot dissociate both.

May be a matter if personality also.

> Is this a good way to present SPARK on Rosetta?
Rightly, at this place, this is moreover a special case: better to show  
what annotations are than to hide it. People aware of SPARK may guess  
implicit parts... other users will not. So better show it explicitly (as  
long as the target is to explain what formal validation means with  
interpretable examples).

At least, I feel it this way. Tell about your comments.