From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,463c5796782db6d8
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 2003-04-11 05:31:22 PST
Path: 
 archiver1.google.com!news1.google.com!newsfeed.stanford.edu!news-spur1.maxwell.syr.edu!news.maxwell.syr.edu!newsfeed.vmunix.org!news2.euro.net!ash.uu.net!spool0900.news.uu.net!reader0902.news.uu.net!not-for-mail
Date: Fri, 11 Apr 2003 08:31:05 -0400
From: Hyman Rosen <hyrosen@mail.com>
User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.0; en-US;
 rv:1.4a) Gecko/20030302
X-Accept-Language: en-us, en
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: [Spark] Arrays of Strings
References: <slrnb95ehu.ob.lutz@taranis.iks-jena.de>
 <1ec946d1.0304090942.3106b4e4@posting.google.com>
 <slrnb9aagi.p2.lutz@taranis.iks-jena.de>
 <1ec946d1.0304100609.52b0fac0@posting.google.com>
 <1049986095.779228@master.nyc.kbcfp.com> <b75n2u$gs8$1@msunews.cl.msu.edu>
In-Reply-To: <b75n2u$gs8$1@msunews.cl.msu.edu>
Content-Type: text/plain; charset=us-ascii; format=flowed
Content-Transfer-Encoding: 7bit
Organization: KBC Financial Products
Message-ID: <1050064265.685430@master.nyc.kbcfp.com>
Cache-Post-Path: master.nyc.kbcfp.com!unknown@fixedcost.nyc.kbcfp.com
X-Cache: nntpcache 3.0.1 (see http://www.nntpcache.org/)
NNTP-Posting-Host: 204.253.250.10
X-Trace: 1050064266 reader2.ash.ops.us.uu.net 27836 204.253.250.10
Xref: archiver1.google.com comp.lang.ada:36086
Date: 2003-04-11T08:31:05-04:00
List-Id: <comp.lang.ada>

Chad R. Meiners wrote:
> You are missing the point of Spark which is to provide a (super)subset of
> Ada in which formal proofs about the implementation are possible.  Lack of
> pointers was not a case of hubris but a deliberate and sound decision in
> Spark's case.  Formal validation and verification methodologies require
> unambiguous specifications and implementations.  Spark is intended to
> satisfy such formal needs.

I think you are demonstrating *my* point. Despite the intentions of Spark,
the OP needs to generate and pass a pointer, and he's desperately trying
to work around the constraints of his programming language. It's all good
and well that you can verify programs written in Spark, but it's not of
much use if programs written in Spark can't do anything!

>>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.
> 
> Of one should know something about a language before one chooses to
> overgeneralize ;)

Do you remember how, in the days of Ada83, it would be suggested that
people use task types and pointers to them to work around the lack of
procedure pointers? Overgeneralize, my foot!