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 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-12 16:51:38 PST Path: archiver1.google.com!news1.google.com!newsfeed.stanford.edu!news.uchicago.edu!newsfeed.cs.wisc.edu!144.212.100.101.MISMATCH!newsfeed!nntp.TheWorld.com!not-for-mail From: Robert A Duff Newsgroups: comp.lang.ada Subject: Re: [Spark] Arrays of Strings Date: 12 Apr 2003 19:51:37 -0400 Organization: The World Public Access UNIX, Brookline, MA Message-ID: References: <1ec946d1.0304090942.3106b4e4@posting.google.com> <1ec946d1.0304100609.52b0fac0@posting.google.com> <1049986095.779228@master.nyc.kbcfp.com> NNTP-Posting-Host: shell01.theworld.com Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: pcls4.std.com 1050191497 29495 199.172.62.241 (12 Apr 2003 23:51:37 GMT) X-Complaints-To: abuse@TheWorld.com NNTP-Posting-Date: Sat, 12 Apr 2003 23:51:37 +0000 (UTC) User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2 Xref: archiver1.google.com comp.lang.ada:36108 Date: 2003-04-12T19:51:37-04:00 List-Id: Hyman Rosen 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