Re: ANN: New technical paper from Ada Europe 2004 now available

[Hyman Rosen <hyrosen@mail.com>]

Peter Amey wrote:
> I don't recall making this claim.  I said that the translation process 
> is "transparent and traceable" and that the C provides a useful 
> intermediate representation for object code verification purposes.  I 
> think these statement stand.
> 
> We certainly wouldn't recommend modification of the C because that 
> immediately throws away all the verification benefits that have been 
> gain by analysing the intermediate SPARK model.
> 
> It is probably true that the C /could/ be maintained if, for example, 
> the translation or SPARK parts of the tool chain were suddenly to become 
> unavailable.

True. But the paper does talk about generating "deliverable" C,
and clearly that C code is meant to be read, not just compiled.
You wouldn't want your target audience, who are presumably expert
in C and already suspicious of using a different language, to be
able to nitpick the way I just did.