Re: [Spark] Arrays of Strings

[Lutz Donnerhacke <lutz@iks-jena.de>]

* Hyman Rosen wrote:
> Whether or not it's reasonable to program in a language without pointers
> is another matter, but I guess if people are happy, more power to them.
> I suspect that a lot of Spark code may wind up using arrays and indexes,
> just like Fortran.

In order to clarify this and finish my part in this discussion, I prefer the
Spark way of programming for two reasons. First I learned, that the failing
proofs point me directly to logical errors in my program, which are
otherwise hard to find, because I can't trigger them (but my users will). So
developing programs with those constraints results in much more stable
programs for me. Second the prohibition of dynamic storage (including
recursion) urges me to look for more efficient algorithms with bounded space
constraints. Due to the fact I'm playing with embedded (or long life)
systems, my code written is Spark is better adopted to my problems than Ada
code.

Of course, there are several points, I'd like to change. Especially user
constraint types (in order to represent dependent types as a single one)
would be fine.

But back to the topic: Rod's idea is right, but does not go far enough. It
requires a dynamically allocated array of pointers or an error message from
the syscall wrapper. Therefore I seperated this part further and use a user
provided space for this purpose.