Re: Ada to 'C' parameter passing problem

[rod.chapman@praxis-cs.co.uk (Rod Chapman)]

mheaney@on2.com (Matthew Heaney) wrote in message news:
> The purpose of a programming language is to make it easy for a
> programmer to write programs.  The language designer should not decide
> by fiat how that should be done.  Both the language and its designer
> should stay out of the programmer's way, and assume that it is the
> programmer himself who is in the best position to decide whether a
> value-returning subprogram is appropriate for the problem at hand.

Aha! I just can't resist steaming back in here...

For high-integrity applications, "ease of writing programs" is
hardly ever the most important thing.  We're really interested in the
ease, efficiency and cost of _verification_ of such programs.  With
that in mind as our primary design goal, then (as a language
designer), we sometimes _do_ remove or constrain language features -
the
lack of function side-effects in SPARK is one such example.

In this case we think it's worth it - the entire data-flow,
information-flow,
and VC-Generation facilities of SPARK depend on this particular
property of the language (and many others...).

We are acutely aware of the trade-off between expressive power and
analysability/verifiability of the language, so we don't take
these decisions lightly.  Matt might find SPARK
too restrictive for his interests and application domain, which is
just fine.  Many of our users think SPARK is about right.  A few of
them think it's too big!  Vive la difference!

All the best,
 Rod