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: g2news2.google.com!news3.google.com!feeder2.cambriumusenet.nl!feed.tweaknews.nl!85.158.31.10.MISMATCH!newsfeed-0.progon.net!progon.net!news-zh.switch.ch!switch.ch!border3.nntp.ams.giganews.com!Xl.tags.giganews.com!border1.nntp.ams.giganews.com!nntp.giganews.com!local2.nntp.ams.giganews.com!nntp.bt.com!news.bt.com.POSTED!not-for-mail NNTP-Posting-Date: Mon, 01 Nov 2010 06:34:43 -0500 From: Brian Drummond Newsgroups: comp.lang.ada Subject: Re: Do people who use Ada also use ocaml or F#? Date: Mon, 01 Nov 2010 11:44:01 +0000 Reply-To: brian@shapes.demon.co.uk Message-ID: <2p9tc6d28od5432e02cq6ot2oojm0pin1j@4ax.com> References: <87k4kz3mda.fsf@mid.deneb.enyo.de> <5jjgrklivesk$.z0is5qe7mgbt.dlg@40tude.net> X-Newsreader: Forte Agent 1.7/32.534 MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-Usenet-Provider: http://www.giganews.com X-AuthenticatedUsername: NoAuthUser X-Trace: sv3-wH7pqwyS1YaQV35QQucWguokl+I4TQvlsI7D7e0M5uAPr/6offB03TDYDWklJ5MtXJppHpllGMXWmqj!/g42ZmDwcBTstVbW7d+LuohSHJ+U9B/T462zy1nswdmcYO69KVbxZvc/V+WxtCA3x++y4xs88YiE!eCw= X-Complaints-To: abuse@btinternet.com X-DMCA-Complaints-To: abuse@btinternet.com X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly X-Postfilter: 1.3.40 X-Original-Bytes: 2574 Xref: g2news2.google.com comp.lang.ada:16067 Date: 2010-11-01T11:44:01+00:00 List-Id: On Sun, 31 Oct 2010 14:46:07 -0700 (PDT), Shark8 wrote: >On Oct 30, 1:37�pm, "Dmitry A. Kazakov" >wrote: >Are generics really non-testable? >I think they are, though perhaps they may quickly spiral into a wide >range of tests. > >The simple example of a bubble-sort on an array is testable: ... > >Because we know that the index is a discrete type, and has the 'Pred & >'Succ functions we can prove this to be correct; and because we are >requiring a function "<" for the element-type we can prove that this >is a correct and complete bubble-sort; it is also a generic function >though. > >Generic > Type Element_Type is private; I think you have argued that it is provable, not testable! Which, given proof tools (Spark-2025, perhaps?) is IMO more desirable, but not quite the same thing... Generics are still infinitely preferable to C++ templates, in which (by instantiating them with new types) I am still finding basic compile time errors in a well-tested example by a vastly more competent C++ programmer than I am, years after it was first used. - Brian