Re: [Spark] Arrays of Strings

[Robert A Duff <bobduff@shell01.TheWorld.com>]

Hyman Rosen <hyrosen@mail.com> writes:

> Matthew Heaney wrote:
> > Doesn't Spark have a #hide clause, to turn off Spark checking?  After
> > all, you're calling a C library function, so what difference does
> > Spark make?
> 
> Getting rid of features that are presumed to cause problems is a bit of
> hubris that language designers always seem to fall victim to. 

As one of the designers of Ada 95, I must say I wholeheartedly agree
with the sentiment here.  Language designers ought to make it easy to
write good programs, not try to make it hard to write bad programs.  Ada
is guilty of the latter in some cases.

However, I think you're being unfair to SPARK here.  SPARK does not say
"you can't do X".  It says, "If you don't do X, then we can prove some
useful properties of your program.  But if you need to do X, then you
can isolate that code, and apply #hide".  That doesn't strike me as
hubris; they're offering you a benefit, in those cases where you can
abide by some restrictions.  You hope that the vast majority of your
code can naturally abide by the restrictions, and isolate the rest in
small packages.

Rod Chapman said it well in another post:

>  The trick with bindings like this is to come up with a package
> specification which is pure SPARK, ...

Non-spark Ada does the same thing in many cases.  Ada does not say, "you
can't do bit-wise type conversions".  Instead it says, "if you want to
do bit-wise conversions, you have to say 'Unchecked_Conversion'".  That
doesn't seem like a restriction to me.  It seems liberating.  It allows
me to have some confidence that the code I'm reading obeys the type
model, so long as I don't see Unchecked_Conversion (or address clauses,
or...).

Contrast with C, where perfectly safe conversions use the same syntax as
potentially troublesome unsafe ones.

My point is:  The language designer should not say "you can't do X"
(assuming X is sometimes useful).  But it's perfectly reasonable for the
language designer to say "if you're going to do X, then you have to say
so".

Back to Hyman:

>...Ada itself
> had a huge problem because the designers thought that function pointers
> could be eliminated.

Agreed.  And C has a huge problem because nested functions are not
allowed.  And both languages (C and Ada) have a huge problem because you
can't pass [pointers to] nested procedures as parameters.

>... Spark gets rid of all pointers, Java gets rid of
> templates, and so on and so on.

I'm not sure Java's lack of templates/generics is due to hubris.
More likely, it's due to trying to [over]simplify the language.

> Then everyone who uses these languages has to figure out how to work
> around the lack of the feature they need, essentially duplicating it in
> some kludgy way. Meanwhile the language designers have their heads in the
> sand and their noses in the air while they pat themselves on the back (:-)
> in self-congratulation on how they have created perfection.

Agreed.

- Bob