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=-0.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: 103376,9e7db243dfa070d7
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII
Path: 
 g2news1.google.com!news4.google.com!proxad.net!feeder1-2.proxad.net!newsfeed.straub-nv.de!newsfeed.utanet.at!newsfeed01.chello.at!newsfeed.arcor.de!newsspool2.arcor-online.net!news.arcor.de.POSTED!not-for-mail
From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Subject: Re: Do people who use Ada also use ocaml or F#?
Newsgroups: comp.lang.ada
User-Agent: 40tude_Dialog/2.0.15.1
MIME-Version: 1.0
Content-Type: text/plain; charset="iso-8859-1"
Content-Transfer-Encoding: 8bit
Reply-To: mailbox@dmitry-kazakov.de
Organization: cbb software GmbH
References: 
 <b17dc7a8-7f8e-46b7-942c-b08ba83ce8fa@j25g2000yqa.googlegroups.com>
 <gt9eaeq2y4pc$.11t5wghh3e8jh$.dlg@40tude.net>
 <87k4kz3mda.fsf@mid.deneb.enyo.de>
 <amlrr4wam4x6.10s9ynz9e8br$.dlg@40tude.net> <op.vlekzab8ule2fv@garhos>
 <5jjgrklivesk$.z0is5qe7mgbt.dlg@40tude.net> <op.vlendwkxule2fv@garhos>
 <1tglk5y57g2ci.cy0cliuo1l3d$.dlg@40tude.net> <op.vlesez1gule2fv@garhos>
Date: Sun, 31 Oct 2010 09:12:27 +0100
Message-ID: <1vhrkzeud47xb$.1ezrevz2un2yt.dlg@40tude.net>
NNTP-Posting-Date: 31 Oct 2010 09:12:28 CET
NNTP-Posting-Host: 1a44f431.newsspool4.arcor-online.net
X-Trace: 
 DXC=7o?hn5\lYl0]E=H1Q9`7874IUK<Cl32<14Fo<]lROoR18kF<OcfhCO;RLAi[OXaNh<[6LHn;2LCV>[<mhadbfdU;FJZ_=ofin^:E;7g:PKVNl0
X-Complaints-To: usenet-abuse@arcor.de
Xref: g2news1.google.com comp.lang.ada:15017
Date: 2010-10-31T09:12:28+01:00
List-Id: <comp.lang.ada>

On Sat, 30 Oct 2010 23:53:13 +0200, Yannick Duch�ne (Hibou57) wrote:

> Le Sat, 30 Oct 2010 22:54:39 +0200, Dmitry A. Kazakov  
> <mailbox@dmitry-kazakov.de> a �crit:
>>> Why should generic usage be provable before instantiation ?
>>
>> Because you want to be able to deliver generic components.
> What would be your requirements to state you are able to deliver a library  
> ? (I mean a library, as a library, not linked to an application).
> 
> Aren't generics similar to libraries ?

to macro libraries

> If you are to deliver a generic as standalone, then there are things you  
> will never be able to prove, right, but just like you will not be able to  
> prove anything for a standalone library you've delivered.

The requirement is that what cannot be proved must be testable. Generics do
not fulfill it. As for provability, note also that generics fail here not
only because normal issues of something being undecidable. The train stops
miles before. Generics lack contracts [*]. You just cannot verify the
behavior since it is not specified. The specifications of Ada generics are
generic.

-------------
* Of course Ada generics have contracts (formal generic parameters etc),
but these exist at the meta language level, useless for checks and tests.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de